Theorem comppfsc 11578

Description: A space where every open cover has a point-finite subcover is compact. This is significant in part because it shows half of the proposition that if only half the generalization in the definition of metacompactness (and consequently paracompactness) is performed, one does not obtain any more spaces.

Hypothesis

Ref	Expression
comppfsc.1	⊢ X = ∪J

Assertion

Ref	Expression
comppfsc	⊢ (J ∈ Top → (J ∈ Comp ↔ ∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d))))

Distinct variable groups:   c,d,J   X,c

Proof of Theorem comppfsc

Step	Hyp	Ref	Expression
1		comppfsc.1	. . . . . . 7 ⊢ X = ∪J
2	1	compcov 11486	. . . . . 6 ⊢ ((J ∈ Comp ⋀ c ⊆ J ⋀ X = ∪c) → ∃d ∈ (℘c ∩ Fin)X = ∪d)
3		finptfin 11568	. . . . . . . . . 10 ⊢ (d ∈ Fin → d ∈ PtFin)
4	3	ad2antlr 405	. . . . . . . . 9 ⊢ (((d ⊆ c ⋀ d ∈ Fin) ⋀ X = ∪d) → d ∈ PtFin)
5		simpll 412	. . . . . . . . 9 ⊢ (((d ⊆ c ⋀ d ∈ Fin) ⋀ X = ∪d) → d ⊆ c)
6		pm3.27 321	. . . . . . . . 9 ⊢ (((d ⊆ c ⋀ d ∈ Fin) ⋀ X = ∪d) → X = ∪d)
7	4, 5, 6	jca32 11341	. . . . . . . 8 ⊢ (((d ⊆ c ⋀ d ∈ Fin) ⋀ X = ∪d) → (d ∈ PtFin ⋀ (d ⊆ c ⋀ X = ∪d)))
8		elin 2259	. . . . . . . . 9 ⊢ (d ∈ (℘c ∩ Fin) ↔ (d ∈ ℘c ⋀ d ∈ Fin))
9		visset 1859	. . . . . . . . . . 11 ⊢ d ∈ V
10	9	elpw 2461	. . . . . . . . . 10 ⊢ (d ∈ ℘c ↔ d ⊆ c)
11	10	anbi1i 484	. . . . . . . . 9 ⊢ ((d ∈ ℘c ⋀ d ∈ Fin) ↔ (d ⊆ c ⋀ d ∈ Fin))
12	8, 11	bitri 171	. . . . . . . 8 ⊢ (d ∈ (℘c ∩ Fin) ↔ (d ⊆ c ⋀ d ∈ Fin))
13	7, 12	sylanb 451	. . . . . . 7 ⊢ ((d ∈ (℘c ∩ Fin) ⋀ X = ∪d) → (d ∈ PtFin ⋀ (d ⊆ c ⋀ X = ∪d)))
14	13	r19.22i2 1779	. . . . . 6 ⊢ (∃d ∈ (℘c ∩ Fin)X = ∪d → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d))
15	2, 14	syl 10	. . . . 5 ⊢ ((J ∈ Comp ⋀ c ⊆ J ⋀ X = ∪c) → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d))
16		visset 1859	. . . . . 6 ⊢ c ∈ V
17	16	elpw 2461	. . . . 5 ⊢ (c ∈ ℘J ↔ c ⊆ J)
18	15, 17	syl3an2b 869	. . . 4 ⊢ ((J ∈ Comp ⋀ c ∈ ℘J ⋀ X = ∪c) → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d))
19	18	3exp 838	. . 3 ⊢ (J ∈ Comp → (c ∈ ℘J → (X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d))))
20	19	r19.21aiv 1759	. 2 ⊢ (J ∈ Comp → ∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)))
21		unieq 2576	. . . . . . . . . . . 12 ⊢ (b = ∅ → ∪b = ∪∅)
22		uni0 2592	. . . . . . . . . . . 12 ⊢ ∪∅ = ∅
23	21, 22	syl6eq 1566	. . . . . . . . . . 11 ⊢ (b = ∅ → ∪b = ∅)
24	23	eqeq2d 1529	. . . . . . . . . 10 ⊢ (b = ∅ → (∪J = ∪b ↔ ∪J = ∅))
25	24	rcla4ev 1923	. . . . . . . . 9 ⊢ ((∅ ∈ (℘a ∩ Fin) ⋀ ∪J = ∅) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b)
26		elin 2259	. . . . . . . . . . 11 ⊢ (∅ ∈ (℘a ∩ Fin) ↔ (∅ ∈ ℘a ⋀ ∅ ∈ Fin))
27		0elpw 2810	. . . . . . . . . . 11 ⊢ ∅ ∈ ℘a
28		emfin 10760	. . . . . . . . . . 11 ⊢ ∅ ∈ Fin
29	26, 27, 28	mpbir2an 735	. . . . . . . . . 10 ⊢ ∅ ∈ (℘a ∩ Fin)
30	29	a1i 8	. . . . . . . . 9 ⊢ (X = ∅ → ∅ ∈ (℘a ∩ Fin))
31	1	eqeq1i 1525	. . . . . . . . . 10 ⊢ (X = ∅ ↔ ∪J = ∅)
32	31	biimpi 149	. . . . . . . . 9 ⊢ (X = ∅ → ∪J = ∅)
33	25, 30, 32	sylanc 473	. . . . . . . 8 ⊢ (X = ∅ → ∃b ∈ (℘a ∩ Fin)∪J = ∪b)
34	33	a1i13 11333	. . . . . . 7 ⊢ ((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) → (X = ∅ → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b)))
35	1	eqeq1i 1525	. . . . . . . . . . . . . . 15 ⊢ (X = ∪a ↔ ∪J = ∪a)
36	35	biimpri 150	. . . . . . . . . . . . . 14 ⊢ (∪J = ∪a → X = ∪a)
37	36	eleq2d 1584	. . . . . . . . . . . . 13 ⊢ (∪J = ∪a → (x ∈ X ↔ x ∈ ∪a))
38	37	biimpd 151	. . . . . . . . . . . 12 ⊢ (∪J = ∪a → (x ∈ X → x ∈ ∪a))
39	38	3ad2ant2 807	. . . . . . . . . . 11 ⊢ ((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) → (x ∈ X → x ∈ ∪a))
40		eluni2 2573	. . . . . . . . . . 11 ⊢ (x ∈ ∪a ↔ ∃s ∈ a x ∈ s)
41	39, 40	syl6ib 210	. . . . . . . . . 10 ⊢ ((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) → (x ∈ X → ∃s ∈ a x ∈ s))
42	36	3ad2ant2 807	. . . . . . . . . . . . . . . . . 18 ⊢ ((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) → X = ∪a)
43	42	adantr 389	. . . . . . . . . . . . . . . . 17 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → X = ∪a)
44		visset 1859	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ s ∈ V
45		visset 1859	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ q ∈ V
46	44, 45	unex 3095	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (s ∪ q) ∈ V
47		eleq2 1578	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (t = (s ∪ q) → (y ∈ t ↔ y ∈ (s ∪ q)))
48		eqeq1 1524	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (t = (s ∪ q) → (t = (s ∪ p) ↔ (s ∪ q) = (s ∪ p)))
49	48	rexbidv 1710	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (t = (s ∪ q) → (∃p ∈ a t = (s ∪ p) ↔ ∃p ∈ a (s ∪ q) = (s ∪ p)))
50	47, 49	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (t = (s ∪ q) → ((y ∈ t ⋀ ∃p ∈ a t = (s ∪ p)) ↔ (y ∈ (s ∪ q) ⋀ ∃p ∈ a (s ∪ q) = (s ∪ p))))
51	46, 50	cla4ev 1915	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((y ∈ (s ∪ q) ⋀ ∃p ∈ a (s ∪ q) = (s ∪ p)) → ∃t(y ∈ t ⋀ ∃p ∈ a t = (s ∪ p)))
52		elun2 2250	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (y ∈ q → y ∈ (s ∪ q))
53	52	ad2antrl 406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (y ∈ q ⋀ q ∈ a)) → y ∈ (s ∪ q))
54		eqid 1518	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (s ∪ q) = (s ∪ q)
55		uneq2 2230	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (p = q → (s ∪ p) = (s ∪ q))
56	55	eqeq2d 1529	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (p = q → ((s ∪ q) = (s ∪ p) ↔ (s ∪ q) = (s ∪ q)))
57	56	rcla4ev 1923	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((q ∈ a ⋀ (s ∪ q) = (s ∪ q)) → ∃p ∈ a (s ∪ q) = (s ∪ p))
58	54, 57	mpan2 700	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (q ∈ a → ∃p ∈ a (s ∪ q) = (s ∪ p))
59	58	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (y ∈ q ⋀ q ∈ a)) → ∃p ∈ a (s ∪ q) = (s ∪ p))
60	51, 53, 59	sylanc 473	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (y ∈ q ⋀ q ∈ a)) → ∃t(y ∈ t ⋀ ∃p ∈ a t = (s ∪ p)))
61	60	ex 371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → ((y ∈ q ⋀ q ∈ a) → ∃t(y ∈ t ⋀ ∃p ∈ a t = (s ∪ p))))
62	61	19.23adv 1251	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (∃q(y ∈ q ⋀ q ∈ a) → ∃t(y ∈ t ⋀ ∃p ∈ a t = (s ∪ p))))
63		eleq2 1578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (t = (s ∪ p) → (y ∈ t ↔ y ∈ (s ∪ p)))
64	63	ad2antrl 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (t = (s ∪ p) ⋀ p ∈ a)) → (y ∈ t ↔ y ∈ (s ∪ p)))
65		elun 2225	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (y ∈ (s ∪ p) ↔ (y ∈ s ⋁ y ∈ p))
66	64, 65	syl6bb 539	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (t = (s ∪ p) ⋀ p ∈ a)) → (y ∈ t ↔ (y ∈ s ⋁ y ∈ p)))
67		eleq2 1578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (q = s → (y ∈ q ↔ y ∈ s))
68		eleq1 1577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (q = s → (q ∈ a ↔ s ∈ a))
69	67, 68	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (q = s → ((y ∈ q ⋀ q ∈ a) ↔ (y ∈ s ⋀ s ∈ a)))
70	44, 69	cla4ev 1915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((y ∈ s ⋀ s ∈ a) → ∃q(y ∈ q ⋀ q ∈ a))
71	70	expcom 372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (s ∈ a → (y ∈ s → ∃q(y ∈ q ⋀ q ∈ a)))
72	71	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((s ∈ a ⋀ x ∈ s) → (y ∈ s → ∃q(y ∈ q ⋀ q ∈ a)))
73	72	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ p ∈ a) → (y ∈ s → ∃q(y ∈ q ⋀ q ∈ a)))
74		visset 1859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ p ∈ V
75		eleq2 1578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (q = p → (y ∈ q ↔ y ∈ p))
76		eleq1 1577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (q = p → (q ∈ a ↔ p ∈ a))
77	75, 76	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (q = p → ((y ∈ q ⋀ q ∈ a) ↔ (y ∈ p ⋀ p ∈ a)))
78	74, 77	cla4ev 1915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((y ∈ p ⋀ p ∈ a) → ∃q(y ∈ q ⋀ q ∈ a))
79	78	expcom 372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (p ∈ a → (y ∈ p → ∃q(y ∈ q ⋀ q ∈ a)))
80	79	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ p ∈ a) → (y ∈ p → ∃q(y ∈ q ⋀ q ∈ a)))
81	73, 80	jaod 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ p ∈ a) → ((y ∈ s ⋁ y ∈ p) → ∃q(y ∈ q ⋀ q ∈ a)))
82	81	adantrl 394	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (t = (s ∪ p) ⋀ p ∈ a)) → ((y ∈ s ⋁ y ∈ p) → ∃q(y ∈ q ⋀ q ∈ a)))
83	66, 82	sylbid 201	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (t = (s ∪ p) ⋀ p ∈ a)) → (y ∈ t → ∃q(y ∈ q ⋀ q ∈ a)))
84	83	exp32 377	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (t = (s ∪ p) → (p ∈ a → (y ∈ t → ∃q(y ∈ q ⋀ q ∈ a)))))
85	84	com23 32	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (p ∈ a → (t = (s ∪ p) → (y ∈ t → ∃q(y ∈ q ⋀ q ∈ a)))))
86	85	r19.23adv 1792	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (∃p ∈ a t = (s ∪ p) → (y ∈ t → ∃q(y ∈ q ⋀ q ∈ a))))
87	86	com23 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (y ∈ t → (∃p ∈ a t = (s ∪ p) → ∃q(y ∈ q ⋀ q ∈ a))))
88	87	imp3a 359	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → ((y ∈ t ⋀ ∃p ∈ a t = (s ∪ p)) → ∃q(y ∈ q ⋀ q ∈ a)))
89	88	19.23adv 1251	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (∃t(y ∈ t ⋀ ∃p ∈ a t = (s ∪ p)) → ∃q(y ∈ q ⋀ q ∈ a)))
90	62, 89	impbid 519	. . . . . . . . . . . . . . . . . . 19 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (∃q(y ∈ q ⋀ q ∈ a) ↔ ∃t(y ∈ t ⋀ ∃p ∈ a t = (s ∪ p))))
91		eluni 2572	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ∈ ∪a ↔ ∃q(y ∈ q ⋀ q ∈ a))
92		eluniab 2579	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ∈ ∪{t∣∃p ∈ a t = (s ∪ p)} ↔ ∃t(y ∈ t ⋀ ∃p ∈ a t = (s ∪ p)))
93	90, 91, 92	3bitr4g 558	. . . . . . . . . . . . . . . . . 18 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (y ∈ ∪a ↔ y ∈ ∪{t∣∃p ∈ a t = (s ∪ p)}))
94	93	eqrdv 1516	. . . . . . . . . . . . . . . . 17 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → ∪a = ∪{t∣∃p ∈ a t = (s ∪ p)})
95	43, 94	eqtrd 1550	. . . . . . . . . . . . . . . 16 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → X = ∪{t∣∃p ∈ a t = (s ∪ p)})
96		simprr 415	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (p ∈ a ⋀ t = (s ∪ p))) → t = (s ∪ p))
97		uniopn 7810	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((J ∈ Top ⋀ {s, p} ⊆ J) → ∪{s, p} ∈ J)
98		3simp1 794	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) → J ∈ Top)
99	98	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (p ∈ a ⋀ t = (s ∪ p))) → J ∈ Top)
100		visset 1859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ a ∈ V
101	100	elpw 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (a ∈ ℘J ↔ a ⊆ J)
102		ssel 2115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (a ⊆ J → (s ∈ a → s ∈ J))
103		ssel 2115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (a ⊆ J → (p ∈ a → p ∈ J))
104	102, 103	anim12d 561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (a ⊆ J → ((s ∈ a ⋀ p ∈ a) → (s ∈ J ⋀ p ∈ J)))
105	104	exp3a 374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (a ⊆ J → (s ∈ a → (p ∈ a → (s ∈ J ⋀ p ∈ J))))
106	101, 105	sylbi 197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (a ∈ ℘J → (s ∈ a → (p ∈ a → (s ∈ J ⋀ p ∈ J))))
107	106	3ad2ant3 808	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) → (s ∈ a → (p ∈ a → (s ∈ J ⋀ p ∈ J))))
108	107	imp31 360	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ s ∈ a) ⋀ p ∈ a) → (s ∈ J ⋀ p ∈ J))
109	108	adantlrr 399	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ p ∈ a) → (s ∈ J ⋀ p ∈ J))
110	109	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (p ∈ a ⋀ t = (s ∪ p))) → (s ∈ J ⋀ p ∈ J))
111	44, 74	prss 2536	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((s ∈ J ⋀ p ∈ J) ↔ {s, p} ⊆ J)
112	110, 111	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (p ∈ a ⋀ t = (s ∪ p))) → {s, p} ⊆ J)
113	97, 99, 112	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (p ∈ a ⋀ t = (s ∪ p))) → ∪{s, p} ∈ J)
114	44, 74	unipr 2581	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪{s, p} = (s ∪ p)
115	113, 114	syl5eqelr 1596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (p ∈ a ⋀ t = (s ∪ p))) → (s ∪ p) ∈ J)
116	96, 115	eqeltrd 1591	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (p ∈ a ⋀ t = (s ∪ p))) → t ∈ J)
117	116	exp32 377	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (p ∈ a → (t = (s ∪ p) → t ∈ J)))
118	117	r19.23adv 1792	. . . . . . . . . . . . . . . . . . 19 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (∃p ∈ a t = (s ∪ p) → t ∈ J))
119	118	abssdv 2173	. . . . . . . . . . . . . . . . . 18 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → {t∣∃p ∈ a t = (s ∪ p)} ⊆ J)
120		elpw2g 2801	. . . . . . . . . . . . . . . . . . . 20 ⊢ (J ∈ Top → ({t∣∃p ∈ a t = (s ∪ p)} ∈ ℘J ↔ {t∣∃p ∈ a t = (s ∪ p)} ⊆ J))
121	120	3ad2ant1 806	. . . . . . . . . . . . . . . . . . 19 ⊢ ((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) → ({t∣∃p ∈ a t = (s ∪ p)} ∈ ℘J ↔ {t∣∃p ∈ a t = (s ∪ p)} ⊆ J))
122	121	adantr 389	. . . . . . . . . . . . . . . . . 18 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → ({t∣∃p ∈ a t = (s ∪ p)} ∈ ℘J ↔ {t∣∃p ∈ a t = (s ∪ p)} ⊆ J))
123	119, 122	mpbird 194	. . . . . . . . . . . . . . . . 17 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → {t∣∃p ∈ a t = (s ∪ p)} ∈ ℘J)
124		unieq 2576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (c = {t∣∃p ∈ a t = (s ∪ p)} → ∪c = ∪{t∣∃p ∈ a t = (s ∪ p)})
125	124	eqeq2d 1529	. . . . . . . . . . . . . . . . . . 19 ⊢ (c = {t∣∃p ∈ a t = (s ∪ p)} → (X = ∪c ↔ X = ∪{t∣∃p ∈ a t = (s ∪ p)}))
126		sseq2 2135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (c = {t∣∃p ∈ a t = (s ∪ p)} → (d ⊆ c ↔ d ⊆ {t∣∃p ∈ a t = (s ∪ p)}))
127	126	anbi1d 620	. . . . . . . . . . . . . . . . . . . 20 ⊢ (c = {t∣∃p ∈ a t = (s ∪ p)} → ((d ⊆ c ⋀ X = ∪d) ↔ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)))
128	127	rexbidv 1710	. . . . . . . . . . . . . . . . . . 19 ⊢ (c = {t∣∃p ∈ a t = (s ∪ p)} → (∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d) ↔ ∃d ∈ PtFin (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)))
129	125, 128	imbi12d 629	. . . . . . . . . . . . . . . . . 18 ⊢ (c = {t∣∃p ∈ a t = (s ∪ p)} → ((X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) ↔ (X = ∪{t∣∃p ∈ a t = (s ∪ p)} → ∃d ∈ PtFin (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d))))
130	129	rcla4v 1919	. . . . . . . . . . . . . . . . 17 ⊢ ({t∣∃p ∈ a t = (s ∪ p)} ∈ ℘J → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → (X = ∪{t∣∃p ∈ a t = (s ∪ p)} → ∃d ∈ PtFin (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d))))
131	123, 130	syl 10	. . . . . . . . . . . . . . . 16 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → (X = ∪{t∣∃p ∈ a t = (s ∪ p)} → ∃d ∈ PtFin (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d))))
132	95, 131	mpid 47	. . . . . . . . . . . . . . 15 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → ∃d ∈ PtFin (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)))
133		elunii 2574	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((x ∈ s ⋀ s ∈ J) → x ∈ ∪J)
134		simprr 415	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → x ∈ s)
135		ssel2 2116	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((a ⊆ J ⋀ s ∈ a) → s ∈ J)
136	135, 101	sylanb 451	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((a ∈ ℘J ⋀ s ∈ a) → s ∈ J)
137	136	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((a ∈ ℘J ⋀ (s ∈ a ⋀ x ∈ s)) → s ∈ J)
138	137	3ad2antl3 817	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → s ∈ J)
139	133, 134, 138	sylanc 473	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → x ∈ ∪J)
140	139	adantr 389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → x ∈ ∪J)
141		simprr 415	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → X = ∪d)
142	141, 1	syl5eqr 1564	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → ∪J = ∪d)
143	140, 142	eleqtrd 1593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → x ∈ ∪d)
144		eqid 1518	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪d = ∪d
145	144	ptfinfin 11569	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((d ∈ PtFin ⋀ x ∈ ∪d) → {z ∈ d∣x ∈ z} ∈ Fin)
146	145	expcom 372	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x ∈ ∪d → (d ∈ PtFin → {z ∈ d∣x ∈ z} ∈ Fin))
147	143, 146	syl 10	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → (d ∈ PtFin → {z ∈ d∣x ∈ z} ∈ Fin))
148		ssel 2115	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} → (z ∈ d → z ∈ {t∣∃p ∈ a t = (s ∪ p)}))
149		eleq2 1578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (z = (s ∪ p) → (x ∈ z ↔ x ∈ (s ∪ p)))
150		elun1 2249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (x ∈ s → x ∈ (s ∪ p))
151	150	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → x ∈ (s ∪ p))
152	149, 151	syl5cbir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (z = (s ∪ p) → x ∈ z))
153	152	a1d 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (p ∈ a → (z = (s ∪ p) → x ∈ z)))
154	153	r19.23adv 1792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (∃p ∈ a z = (s ∪ p) → x ∈ z))
155		visset 1859	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ z ∈ V
156		eqeq1 1524	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (t = z → (t = (s ∪ p) ↔ z = (s ∪ p)))
157	156	rexbidv 1710	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (t = z → (∃p ∈ a t = (s ∪ p) ↔ ∃p ∈ a z = (s ∪ p)))
158	155, 157	elab 1943	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (z ∈ {t∣∃p ∈ a t = (s ∪ p)} ↔ ∃p ∈ a z = (s ∪ p))
159	154, 158	syl5ib 204	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (z ∈ {t∣∃p ∈ a t = (s ∪ p)} → x ∈ z))
160	148, 159	sylan9r 471	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ d ⊆ {t∣∃p ∈ a t = (s ∪ p)}) → (z ∈ d → x ∈ z))
161	160	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → (z ∈ d → x ∈ z))
162	161	r19.21aiv 1759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → ∀z ∈ d x ∈ z)
163		ssid 2132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ d ⊆ d
164	162, 163	jctil 290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → (d ⊆ d ⋀ ∀z ∈ d x ∈ z))
165		ssrab 2177	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (d ⊆ {z ∈ d∣x ∈ z} ↔ (d ⊆ d ⋀ ∀z ∈ d x ∈ z))
166	164, 165	sylibr 198	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → d ⊆ {z ∈ d∣x ∈ z})
167		ssfi 4683	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (({z ∈ d∣x ∈ z} ∈ Fin ⋀ d ⊆ {z ∈ d∣x ∈ z}) → d ∈ Fin)
168	167	expcom 372	. . . . . . . . . . . . . . . . . . . 20 ⊢ (d ⊆ {z ∈ d∣x ∈ z} → ({z ∈ d∣x ∈ z} ∈ Fin → d ∈ Fin))
169	166, 168	syl 10	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → ({z ∈ d∣x ∈ z} ∈ Fin → d ∈ Fin))
170		ssel 2115	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} → (q ∈ d → q ∈ {t∣∃p ∈ a t = (s ∪ p)}))
171		eqeq1 1524	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (t = q → (t = (s ∪ p) ↔ q = (s ∪ p)))
172	171	rexbidv 1710	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (t = q → (∃p ∈ a t = (s ∪ p) ↔ ∃p ∈ a q = (s ∪ p)))
173	45, 172	elab 1943	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (q ∈ {t∣∃p ∈ a t = (s ∪ p)} ↔ ∃p ∈ a q = (s ∪ p))
174	170, 173	syl6ib 210	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} → (q ∈ d → ∃p ∈ a q = (s ∪ p)))
175	174	r19.21aiv 1759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} → ∀q ∈ d ∃p ∈ a q = (s ∪ p))
176	175	ad2antrl 406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → ∀q ∈ d ∃p ∈ a q = (s ∪ p))
177		uneq2 2230	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (p = (f ‘q) → (s ∪ p) = (s ∪ (f ‘q)))
178	177	eqeq2d 1529	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (p = (f ‘q) → (q = (s ∪ p) ↔ q = (s ∪ (f ‘q))))
179	178	ac6sfi 4591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((d ∈ Fin ⋀ ∀q ∈ d ∃p ∈ a q = (s ∪ p)) → ∃f(f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))
180	179	expcom 372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀q ∈ d ∃p ∈ a q = (s ∪ p) → (d ∈ Fin → ∃f(f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q)))))
181	176, 180	syl 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → (d ∈ Fin → ∃f(f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q)))))
182		unieq 2576	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (b = (ran f ∪ {s}) → ∪b = ∪(ran f ∪ {s}))
183	182	eqeq2d 1529	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (b = (ran f ∪ {s}) → (∪J = ∪b ↔ ∪J = ∪(ran f ∪ {s})))
184	183	rcla4ev 1923	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ran f ∪ {s}) ∈ (℘a ∩ Fin) ⋀ ∪J = ∪(ran f ∪ {s})) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b)
185		frn 3740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (f:d–→a → ran f ⊆ a)
186	185	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))) → ran f ⊆ a)
187	186	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → ran f ⊆ a)
188		snssi 2530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (s ∈ a → {s} ⊆ a)
189	188	ad2antrl 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → {s} ⊆ a)
190	189	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → {s} ⊆ a)
191	187, 190	jca 286	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → (ran f ⊆ a ⋀ {s} ⊆ a))
192		unss 2256	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ran f ⊆ a ⋀ {s} ⊆ a) ↔ (ran f ∪ {s}) ⊆ a)
193	191, 192	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → (ran f ∪ {s}) ⊆ a)
194		domfi 4684	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((d ∈ Fin ⋀ ran f ≼ d) → ran f ∈ Fin)
195		simprl 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → d ∈ Fin)
196		fodomfi 4709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((d ∈ Fin ⋀ f:d–onto→ran f) → ran f ≼ d)
197		ffn 3734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (f:d–→a → f Fn d)
198		dffn4 3785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (f Fn d ↔ f:d–onto→ran f)
199	197, 198	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (f:d–→a → f:d–onto→ran f)
200	199	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))) → f:d–onto→ran f)
201	200	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → f:d–onto→ran f)
202	196, 195, 201	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → ran f ≼ d)
203	194, 195, 202	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → ran f ∈ Fin)
204		snfi 4573	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {s} ∈ Fin
205		unfi 4697	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ran f ∈ Fin ⋀ {s} ∈ Fin) → (ran f ∪ {s}) ∈ Fin)
206	204, 205	mpan2 700	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ran f ∈ Fin → (ran f ∪ {s}) ∈ Fin)
207	203, 206	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → (ran f ∪ {s}) ∈ Fin)
208	193, 207	jca 286	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → ((ran f ∪ {s}) ⊆ a ⋀ (ran f ∪ {s}) ∈ Fin))
209		elin 2259	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ran f ∪ {s}) ∈ (℘a ∩ Fin) ↔ ((ran f ∪ {s}) ∈ ℘a ⋀ (ran f ∪ {s}) ∈ Fin))
210	100	elpw2 2802	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ran f ∪ {s}) ∈ ℘a ↔ (ran f ∪ {s}) ⊆ a)
211	210	anbi1i 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ran f ∪ {s}) ∈ ℘a ⋀ (ran f ∪ {s}) ∈ Fin) ↔ ((ran f ∪ {s}) ⊆ a ⋀ (ran f ∪ {s}) ∈ Fin))
212	209, 211	bitri 171	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ran f ∪ {s}) ∈ (℘a ∩ Fin) ↔ ((ran f ∪ {s}) ⊆ a ⋀ (ran f ∪ {s}) ∈ Fin))
213	208, 212	sylibr 198	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → (ran f ∪ {s}) ∈ (℘a ∩ Fin))
214		simplrr 11365	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → X = ∪d)
215	214, 1	syl5eqr 1564	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → ∪J = ∪d)
216		id 59	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (q = z → q = z)
217		fveq2 3835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (q = z → (f ‘q) = (f ‘z))
218	217	uneq2d 2236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (q = z → (s ∪ (f ‘q)) = (s ∪ (f ‘z)))
219	216, 218	eqeq12d 1532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (q = z → (q = (s ∪ (f ‘q)) ↔ z = (s ∪ (f ‘z))))
220	219	rcla4cv 1920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∀q ∈ d q = (s ∪ (f ‘q)) → (z ∈ d → z = (s ∪ (f ‘z))))
221	220	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))) → (z ∈ d → z = (s ∪ (f ‘z))))
222	221	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → (z ∈ d → z = (s ∪ (f ‘z))))
223		eleq2 1578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (z = (s ∪ (f ‘z)) → (y ∈ z ↔ y ∈ (s ∪ (f ‘z))))
224	223	imbi1d 616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (z = (s ∪ (f ‘z)) → ((y ∈ z → y ∈ ∪(ran f ∪ {s})) ↔ (y ∈ (s ∪ (f ‘z)) → y ∈ ∪(ran f ∪ {s}))))
225	44	snid 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ s ∈ {s}
226		elun2 2250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (s ∈ {s} → s ∈ (ran f ∪ {s}))
227	225, 226	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ s ∈ (ran f ∪ {s})
228		elunii 2574	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((y ∈ s ⋀ s ∈ (ran f ∪ {s})) → y ∈ ∪(ran f ∪ {s}))
229	227, 228	mpan2 700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (y ∈ s → y ∈ ∪(ran f ∪ {s}))
230	229	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) ⋀ z ∈ d) → (y ∈ s → y ∈ ∪(ran f ∪ {s})))
231		fnfvelrn 3927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((f Fn d ⋀ z ∈ d) → (f ‘z) ∈ ran f)
232	231	ex 371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (f Fn d → (z ∈ d → (f ‘z) ∈ ran f))
233		elunii 2574	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((y ∈ (f ‘z) ⋀ (f ‘z) ∈ ran f) → y ∈ ∪ran f)
234		ssun1 2245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ran f ⊆ (ran f ∪ {s})
235		uniss 2588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (ran f ⊆ (ran f ∪ {s}) → ∪ran f ⊆ ∪(ran f ∪ {s}))
236	234, 235	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ∪ran f ⊆ ∪(ran f ∪ {s})
237	236	sseli 2117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (y ∈ ∪ran f → y ∈ ∪(ran f ∪ {s}))
238	233, 237	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((y ∈ (f ‘z) ⋀ (f ‘z) ∈ ran f) → y ∈ ∪(ran f ∪ {s}))
239	238	expcom 372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((f ‘z) ∈ ran f → (y ∈ (f ‘z) → y ∈ ∪(ran f ∪ {s})))
240	232, 239	syl6 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (f Fn d → (z ∈ d → (y ∈ (f ‘z) → y ∈ ∪(ran f ∪ {s}))))
241	197, 240	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (f:d–→a → (z ∈ d → (y ∈ (f ‘z) → y ∈ ∪(ran f ∪ {s}))))
242	241	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))) → (z ∈ d → (y ∈ (f ‘z) → y ∈ ∪(ran f ∪ {s}))))
243	242	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → (z ∈ d → (y ∈ (f ‘z) → y ∈ ∪(ran f ∪ {s}))))
244	243	imp 348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) ⋀ z ∈ d) → (y ∈ (f ‘z) → y ∈ ∪(ran f ∪ {s})))
245	230, 244	jaod 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) ⋀ z ∈ d) → ((y ∈ s ⋁ y ∈ (f ‘z)) → y ∈ ∪(ran f ∪ {s})))
246		elun 2225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (y ∈ (s ∪ (f ‘z)) ↔ (y ∈ s ⋁ y ∈ (f ‘z)))
247	245, 246	syl5ib 204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) ⋀ z ∈ d) → (y ∈ (s ∪ (f ‘z)) → y ∈ ∪(ran f ∪ {s})))
248	224, 247	syl5cbir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) ⋀ z ∈ d) → (z = (s ∪ (f ‘z)) → (y ∈ z → y ∈ ∪(ran f ∪ {s}))))
249	248	ex 371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → (z ∈ d → (z = (s ∪ (f ‘z)) → (y ∈ z → y ∈ ∪(ran f ∪ {s})))))
250	222, 249	mpdd 46	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → (z ∈ d → (y ∈ z → y ∈ ∪(ran f ∪ {s}))))
251	250	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → (y ∈ z → (z ∈ d → y ∈ ∪(ran f ∪ {s}))))
252	251	imp3a 359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → ((y ∈ z ⋀ z ∈ d) → y ∈ ∪(ran f ∪ {s})))
253	252	19.23adv 1251	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → (∃z(y ∈ z ⋀ z ∈ d) → y ∈ ∪(ran f ∪ {s})))
254		eluni 2572	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (y ∈ ∪d ↔ ∃z(y ∈ z ⋀ z ∈ d))
255	253, 254	syl5ib 204	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → (y ∈ ∪d → y ∈ ∪(ran f ∪ {s})))
256	255	ssrdv 2122	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → ∪d ⊆ ∪(ran f ∪ {s}))
257	215, 256	eqsstrd 2147	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → ∪J ⊆ ∪(ran f ∪ {s}))
258		elpwi 2463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (a ∈ ℘J → a ⊆ J)
259	258	3ad2ant3 808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) → a ⊆ J)
260	259	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → a ⊆ J)
261	260	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → a ⊆ J)
262	187, 261	sstrd 2126	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → ran f ⊆ J)
263		snssi 2530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (s ∈ J → {s} ⊆ J)
264	135, 263	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((a ⊆ J ⋀ s ∈ a) → {s} ⊆ J)
265	264, 101	sylanb 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((a ∈ ℘J ⋀ s ∈ a) → {s} ⊆ J)
266	265	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((a ∈ ℘J ⋀ (s ∈ a ⋀ x ∈ s)) → {s} ⊆ J)
267	266	3ad2antl3 817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → {s} ⊆ J)
268	267	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → {s} ⊆ J)
269	262, 268	jca 286	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → (ran f ⊆ J ⋀ {s} ⊆ J))
270		unss 2256	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ran f ⊆ J ⋀ {s} ⊆ J) ↔ (ran f ∪ {s}) ⊆ J)
271	269, 270	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → (ran f ∪ {s}) ⊆ J)
272		uniss 2588	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ran f ∪ {s}) ⊆ J → ∪(ran f ∪ {s}) ⊆ ∪J)
273	271, 272	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → ∪(ran f ∪ {s}) ⊆ ∪J)
274	257, 273	eqssd 2131	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → ∪J = ∪(ran f ∪ {s}))
275	184, 213, 274	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ (d ∈ Fin ⋀ (f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))))) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b)
276	275	expr 11361	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ d ∈ Fin) → ((f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b))
277	276	19.23adv 1251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) ⋀ d ∈ Fin) → (∃f(f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b))
278	277	ex 371	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → (d ∈ Fin → (∃f(f:d–→a ⋀ ∀q ∈ d q = (s ∪ (f ‘q))) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b)))
279	181, 278	mpdd 46	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → (d ∈ Fin → ∃b ∈ (℘a ∩ Fin)∪J = ∪b))
280	147, 169, 279	3syld 11324	. . . . . . . . . . . . . . . . . 18 ⊢ ((((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) ⋀ (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d)) → (d ∈ PtFin → ∃b ∈ (℘a ∩ Fin)∪J = ∪b))
281	280	ex 371	. . . . . . . . . . . . . . . . 17 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → ((d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d) → (d ∈ PtFin → ∃b ∈ (℘a ∩ Fin)∪J = ∪b)))
282	281	com23 32	. . . . . . . . . . . . . . . 16 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (d ∈ PtFin → ((d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b)))
283	282	r19.23adv 1792	. . . . . . . . . . . . . . 15 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (∃d ∈ PtFin (d ⊆ {t∣∃p ∈ a t = (s ∪ p)} ⋀ X = ∪d) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b))
284	132, 283	syld 27	. . . . . . . . . . . . . 14 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ (s ∈ a ⋀ x ∈ s)) → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b))
285	284	exp32 377	. . . . . . . . . . . . 13 ⊢ ((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) → (s ∈ a → (x ∈ s → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b))))
286	285	adantr 389	. . . . . . . . . . . 12 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ x ∈ X) → (s ∈ a → (x ∈ s → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b))))
287	286	r19.23adv 1792	. . . . . . . . . . 11 ⊢ (((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) ⋀ x ∈ X) → (∃s ∈ a x ∈ s → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b)))
288	287	ex 371	. . . . . . . . . 10 ⊢ ((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) → (x ∈ X → (∃s ∈ a x ∈ s → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b))))
289	41, 288	mpdd 46	. . . . . . . . 9 ⊢ ((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) → (x ∈ X → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b)))
290	289	19.23adv 1251	. . . . . . . 8 ⊢ ((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) → (∃x x ∈ X → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b)))
291		n0 2341	. . . . . . . 8 ⊢ (X ≠ ∅ ↔ ∃x x ∈ X)
292	290, 291	syl5ib 204	. . . . . . 7 ⊢ ((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) → (X ≠ ∅ → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b)))
293	34, 292	pm2.61dne 1681	. . . . . 6 ⊢ ((J ∈ Top ⋀ ∪J = ∪a ⋀ a ∈ ℘J) → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b))
294	293	3exp 838	. . . . 5 ⊢ (J ∈ Top → (∪J = ∪a → (a ∈ ℘J → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → ∃b ∈ (℘a ∩ Fin)∪J = ∪b))))
295	294	com24 37	. . . 4 ⊢ (J ∈ Top → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → (a ∈ ℘J → (∪J = ∪a → ∃b ∈ (℘a ∩ Fin)∪J = ∪b))))
296	295	r19.21adv 1764	. . 3 ⊢ (J ∈ Top → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → ∀a ∈ ℘ J(∪J = ∪a → ∃b ∈ (℘a ∩ Fin)∪J = ∪b)))
297		iscomp 11114	. . . 4 ⊢ (J ∈ Comp ↔ (J ∈ Top ⋀ ∀a ∈ ℘ J(∪J = ∪a → ∃b ∈ (℘a ∩ Fin)∪J = ∪b)))
298	297	baibr 690	. . 3 ⊢ (J ∈ Top → (∀a ∈ ℘ J(∪J = ∪a → ∃b ∈ (℘a ∩ Fin)∪J = ∪b) ↔ J ∈ Comp))
299	296, 298	sylibd 200	. 2 ⊢ (J ∈ Top → (∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d)) → J ∈ Comp))
300	20, 299	impbid2 521	1 ⊢ (J ∈ Top → (J ∈ Comp ↔ ∀c ∈ ℘ J(X = ∪c → ∃d ∈ PtFin (d ⊆ c ⋀ X = ∪d))))

Syntax hints:   → wi 3   ↔ wb 144   ⋁ wo 220   ⋀ wa 221   ⋀ w3a 781   = wceq 992   ∈ wcel 994  ∃wex 1016  {cab 1505   ≠ wne 1628  ∀wral 1691  ∃wrex 1692  {crab 1694   ∪ cun 2097   ∩ cin 2098   ⊆ wss 2099  ∅c0 2332  ℘cpw 2458  {csn 2467  {cpr 2468  ∪cuni 2569   class class class wbr 2692  ran crn 3252   Fn wfn 3258  –→wf 3259  –onto→wfo 3261   ‘cfv 3263   ≼ cdom 4506  Fincfn 4508  Topctop 7800  Compccomp 11112  PtFincptfin 11520

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-reu 1697  df-rab 1698  df-v 1858  df-sbc 1987  df-csb 2052  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-pss 2107  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-int 2601  df-iun 2635  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-lim 2980  df-suc 2981  df-om 3219  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-fv 3279  df-opr 4023  df-oprab 4024  df-rdg 4233  df-1o 4269  df-oadd 4271  df-er 4401  df-en 4509  df-dom 4510  df-fin 4512  df-top 7804  df-comp 11113  df-ptfin 11526

Copyright terms: Public domain