compsub - Mathbox for Jeff Hankins

Mathbox for Jeff Hankins

< Previous Next >
Related theorems
GIF version

Theorem compsub 11481

Description: Two equivalent ways of describing a compact subset of a topological space. Inspired by Sue E. Goodman's Beginning Topology.

**Hypothesis**
Ref	Expression
compsub.1	⊢ X = ∪J

**Assertion**
Ref	Expression
compsub	⊢ ((J ∈ Top ⋀ S ⊆ X) → ((subSp ‘S, J) ∈ Comp ↔ ∀c ∈ ℘ J(S ⊆ ∪c → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d)))

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

**Proof of Theorem compsub**
Step	Hyp	Ref	Expression
1		stoig3 11057	. . . . 5 ⊢ ((J ∈ Top ⋀ S ⊆ ∪J) → (subSp ‘S, J) ∈ Top)
2		compsub.1	. . . . . 6 ⊢ X = ∪J
3	2	sseq2i 2138	. . . . 5 ⊢ (S ⊆ X ↔ S ⊆ ∪J)
4	1, 3	sylan2b 454	. . . 4 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (subSp ‘S, J) ∈ Top)
5		ibar 646	. . . . 5 ⊢ ((subSp ‘S, J) ∈ Top → (∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t) ↔ ((subSp ‘S, J) ∈ Top ⋀ ∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t))))
6	5	bicomd 524	. . . 4 ⊢ ((subSp ‘S, J) ∈ Top → (((subSp ‘S, J) ∈ Top ⋀ ∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t)) ↔ ∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t)))
7	4, 6	syl 10	. . 3 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (((subSp ‘S, J) ∈ Top ⋀ ∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t)) ↔ ∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t)))
8		iscomp 11107	. . 3 ⊢ ((subSp ‘S, J) ∈ Comp ↔ ((subSp ‘S, J) ∈ Top ⋀ ∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t)))
9	7, 8	syl5bb 535	. 2 ⊢ ((J ∈ Top ⋀ S ⊆ X) → ((subSp ‘S, J) ∈ Comp ↔ ∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t)))
10		unieq 2576	. . . . . . . . . 10 ⊢ (s = {x∣∃y ∈ c x = (y ∩ S)} → ∪s = ∪{x∣∃y ∈ c x = (y ∩ S)})
11	10	eqeq2d 1529	. . . . . . . . 9 ⊢ (s = {x∣∃y ∈ c x = (y ∩ S)} → (∪(subSp ‘S, J) = ∪s ↔ ∪(subSp ‘S, J) = ∪{x∣∃y ∈ c x = (y ∩ S)}))
12		pweq 2460	. . . . . . . . . . 11 ⊢ (s = {x∣∃y ∈ c x = (y ∩ S)} → ℘s = ℘{x∣∃y ∈ c x = (y ∩ S)})
13	12	ineq1d 2268	. . . . . . . . . 10 ⊢ (s = {x∣∃y ∈ c x = (y ∩ S)} → (℘s ∩ Fin) = (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin))
14	13	rexeq1d 1836	. . . . . . . . 9 ⊢ (s = {x∣∃y ∈ c x = (y ∩ S)} → (∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t ↔ ∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)∪(subSp ‘S, J) = ∪t))
15	11, 14	imbi12d 629	. . . . . . . 8 ⊢ (s = {x∣∃y ∈ c x = (y ∩ S)} → ((∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t) ↔ (∪(subSp ‘S, J) = ∪{x∣∃y ∈ c x = (y ∩ S)} → ∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)∪(subSp ‘S, J) = ∪t)))
16	15	rcla4va 1921	. . . . . . 7 ⊢ (({x∣∃y ∈ c x = (y ∩ S)} ∈ ℘(subSp ‘S, J) ⋀ ∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t)) → (∪(subSp ‘S, J) = ∪{x∣∃y ∈ c x = (y ∩ S)} → ∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)∪(subSp ‘S, J) = ∪t))
17		visset 1859	. . . . . . . . . . . . . . 15 ⊢ c ∈ V
18	17	elpw 2461	. . . . . . . . . . . . . 14 ⊢ (c ∈ ℘J ↔ c ⊆ J)
19		ssel2 2116	. . . . . . . . . . . . . . . 16 ⊢ ((c ⊆ J ⋀ y ∈ c) → y ∈ J)
20		ineq1 2262	. . . . . . . . . . . . . . . . . . 19 ⊢ (d = y → (d ∩ S) = (y ∩ S))
21	20	eqeq2d 1529	. . . . . . . . . . . . . . . . . 18 ⊢ (d = y → (t = (d ∩ S) ↔ t = (y ∩ S)))
22	21	rcla4ev 1923	. . . . . . . . . . . . . . . . 17 ⊢ ((y ∈ J ⋀ t = (y ∩ S)) → ∃d ∈ J t = (d ∩ S))
23	22	ex 371	. . . . . . . . . . . . . . . 16 ⊢ (y ∈ J → (t = (y ∩ S) → ∃d ∈ J t = (d ∩ S)))
24	19, 23	syl 10	. . . . . . . . . . . . . . 15 ⊢ ((c ⊆ J ⋀ y ∈ c) → (t = (y ∩ S) → ∃d ∈ J t = (d ∩ S)))
25	24	ex 371	. . . . . . . . . . . . . 14 ⊢ (c ⊆ J → (y ∈ c → (t = (y ∩ S) → ∃d ∈ J t = (d ∩ S))))
26	18, 25	sylbi 197	. . . . . . . . . . . . 13 ⊢ (c ∈ ℘J → (y ∈ c → (t = (y ∩ S) → ∃d ∈ J t = (d ∩ S))))
27	26	adantl 388	. . . . . . . . . . . 12 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) → (y ∈ c → (t = (y ∩ S) → ∃d ∈ J t = (d ∩ S))))
28	27	r19.23adv 1792	. . . . . . . . . . 11 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) → (∃y ∈ c t = (y ∩ S) → ∃d ∈ J t = (d ∩ S)))
29		issubspt 11050	. . . . . . . . . . . 12 ⊢ ((J ∈ Top ⋀ t ∈ V ⋀ S ∈ V) → (t ∈ (subSp ‘S, J) ↔ ∃d ∈ J t = (d ∩ S)))
30		simpll 412	. . . . . . . . . . . 12 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) → J ∈ Top)
31		visset 1859	. . . . . . . . . . . . 13 ⊢ t ∈ V
32	31	a1i 8	. . . . . . . . . . . 12 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) → t ∈ V)
33		ssexg 2795	. . . . . . . . . . . . . . . 16 ⊢ ((S ⊆ ∪J ⋀ ∪J ∈ V) → S ∈ V)
34		uniexg 3094	. . . . . . . . . . . . . . . 16 ⊢ (J ∈ Top → ∪J ∈ V)
35	33, 34	sylan2 453	. . . . . . . . . . . . . . 15 ⊢ ((S ⊆ ∪J ⋀ J ∈ Top) → S ∈ V)
36	35	ancoms 438	. . . . . . . . . . . . . 14 ⊢ ((J ∈ Top ⋀ S ⊆ ∪J) → S ∈ V)
37	36, 3	sylan2b 454	. . . . . . . . . . . . 13 ⊢ ((J ∈ Top ⋀ S ⊆ X) → S ∈ V)
38	37	adantr 389	. . . . . . . . . . . 12 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) → S ∈ V)
39	29, 30, 32, 38	syl3anc 864	. . . . . . . . . . 11 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) → (t ∈ (subSp ‘S, J) ↔ ∃d ∈ J t = (d ∩ S)))
40	28, 39	sylibrd 202	. . . . . . . . . 10 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) → (∃y ∈ c t = (y ∩ S) → t ∈ (subSp ‘S, J)))
41		eqeq1 1524	. . . . . . . . . . . 12 ⊢ (x = t → (x = (y ∩ S) ↔ t = (y ∩ S)))
42	41	rexbidv 1710	. . . . . . . . . . 11 ⊢ (x = t → (∃y ∈ c x = (y ∩ S) ↔ ∃y ∈ c t = (y ∩ S)))
43	31, 42	elab 1943	. . . . . . . . . 10 ⊢ (t ∈ {x∣∃y ∈ c x = (y ∩ S)} ↔ ∃y ∈ c t = (y ∩ S))
44	40, 43	syl5ib 204	. . . . . . . . 9 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) → (t ∈ {x∣∃y ∈ c x = (y ∩ S)} → t ∈ (subSp ‘S, J)))
45	44	ssrdv 2122	. . . . . . . 8 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) → {x∣∃y ∈ c x = (y ∩ S)} ⊆ (subSp ‘S, J))
46	17	abrexex 3974	. . . . . . . . 9 ⊢ {x∣∃y ∈ c x = (y ∩ S)} ∈ V
47	46	elpw 2461	. . . . . . . 8 ⊢ ({x∣∃y ∈ c x = (y ∩ S)} ∈ ℘(subSp ‘S, J) ↔ {x∣∃y ∈ c x = (y ∩ S)} ⊆ (subSp ‘S, J))
48	45, 47	sylibr 198	. . . . . . 7 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) → {x∣∃y ∈ c x = (y ∩ S)} ∈ ℘(subSp ‘S, J))
49	16, 48	sylan 450	. . . . . 6 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ ∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t)) → (∪(subSp ‘S, J) = ∪{x∣∃y ∈ c x = (y ∩ S)} → ∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)∪(subSp ‘S, J) = ∪t))
50	49	ex 371	. . . . 5 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) → (∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t) → (∪(subSp ‘S, J) = ∪{x∣∃y ∈ c x = (y ∩ S)} → ∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)∪(subSp ‘S, J) = ∪t)))
51		stoig2 11056	. . . . . . . . . . . 12 ⊢ ((J ∈ Top ⋀ S ⊆ ∪J) → ∪(subSp ‘S, J) = S)
52	51, 3	sylan2b 454	. . . . . . . . . . 11 ⊢ ((J ∈ Top ⋀ S ⊆ X) → ∪(subSp ‘S, J) = S)
53	52	ad2antrr 404	. . . . . . . . . 10 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → ∪(subSp ‘S, J) = S)
54		visset 1859	. . . . . . . . . . . . . . 15 ⊢ y ∈ V
55	54	inex1 2790	. . . . . . . . . . . . . 14 ⊢ (y ∩ S) ∈ V
56	55	dfiun2 2655	. . . . . . . . . . . . 13 ⊢ ∪y ∈ c (y ∩ S) = ∪{x∣∃y ∈ c x = (y ∩ S)}
57	56	eqcomi 1522	. . . . . . . . . . . 12 ⊢ ∪{x∣∃y ∈ c x = (y ∩ S)} = ∪y ∈ c (y ∩ S)
58	57	a1i 8	. . . . . . . . . . 11 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → ∪{x∣∃y ∈ c x = (y ∩ S)} = ∪y ∈ c (y ∩ S))
59		incom 2260	. . . . . . . . . . . . 13 ⊢ (y ∩ S) = (S ∩ y)
60	59	a1i 8	. . . . . . . . . . . 12 ⊢ (((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ y ∈ c) → (y ∩ S) = (S ∩ y))
61	60	iuneq2dv 2650	. . . . . . . . . . 11 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → ∪y ∈ c (y ∩ S) = ∪y ∈ c (S ∩ y))
62		iunin2 2677	. . . . . . . . . . . . 13 ⊢ ∪y ∈ c (S ∩ y) = (S ∩ ∪y ∈ c y)
63	62	a1i 8	. . . . . . . . . . . 12 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → ∪y ∈ c (S ∩ y) = (S ∩ ∪y ∈ c y))
64		uniiun 2669	. . . . . . . . . . . . . . 15 ⊢ ∪c = ∪y ∈ c y
65	64	eqcomi 1522	. . . . . . . . . . . . . 14 ⊢ ∪y ∈ c y = ∪c
66	65	a1i 8	. . . . . . . . . . . . 13 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → ∪y ∈ c y = ∪c)
67	66	ineq2d 2269	. . . . . . . . . . . 12 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → (S ∩ ∪y ∈ c y) = (S ∩ ∪c))
68		sseqin2 2281	. . . . . . . . . . . . . . 15 ⊢ (S ⊆ ∪c ↔ (∪c ∩ S) = S)
69	68	biimpi 149	. . . . . . . . . . . . . 14 ⊢ (S ⊆ ∪c → (∪c ∩ S) = S)
70		incom 2260	. . . . . . . . . . . . . 14 ⊢ (S ∩ ∪c) = (∪c ∩ S)
71	69, 70	syl5eq 1562	. . . . . . . . . . . . 13 ⊢ (S ⊆ ∪c → (S ∩ ∪c) = S)
72	71	adantl 388	. . . . . . . . . . . 12 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → (S ∩ ∪c) = S)
73	63, 67, 72	3eqtrd 1554	. . . . . . . . . . 11 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → ∪y ∈ c (S ∩ y) = S)
74	58, 61, 73	3eqtrd 1554	. . . . . . . . . 10 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → ∪{x∣∃y ∈ c x = (y ∩ S)} = S)
75	53, 74	eqeq12d 1532	. . . . . . . . 9 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → (∪(subSp ‘S, J) = ∪{x∣∃y ∈ c x = (y ∩ S)} ↔ S = S))
76	53	eqeq1d 1526	. . . . . . . . . 10 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → (∪(subSp ‘S, J) = ∪t ↔ S = ∪t))
77	76	rexbidv 1710	. . . . . . . . 9 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → (∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)∪(subSp ‘S, J) = ∪t ↔ ∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)S = ∪t))
78	75, 77	imbi12d 629	. . . . . . . 8 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → ((∪(subSp ‘S, J) = ∪{x∣∃y ∈ c x = (y ∩ S)} → ∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)∪(subSp ‘S, J) = ∪t) ↔ (S = S → ∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)S = ∪t)))
79		ineq1 2262	. . . . . . . . . . . . . . . 16 ⊢ (y = (f ‘s) → (y ∩ S) = ((f ‘s) ∩ S))
80	79	eqeq2d 1529	. . . . . . . . . . . . . . 15 ⊢ (y = (f ‘s) → (s = (y ∩ S) ↔ s = ((f ‘s) ∩ S)))
81	80	ac6sfi 4591	. . . . . . . . . . . . . 14 ⊢ ((t ∈ Fin ⋀ ∀s ∈ t ∃y ∈ c s = (y ∩ S)) → ∃f(f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S)))
82	81	ancoms 438	. . . . . . . . . . . . 13 ⊢ ((∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin) → ∃f(f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S)))
83	82	adantl 388	. . . . . . . . . . . 12 ⊢ (((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) → ∃f(f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S)))
84		frn 3740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f:t–→c → ran f ⊆ c)
85	84	ad2antrl 406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) ⋀ S = ∪t) ⋀ (f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S))) → ran f ⊆ c)
86		visset 1859	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ f ∈ V
87	86	rnex 3448	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ran f ∈ V
88	87	elpw 2461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ran f ∈ ℘c ↔ ran f ⊆ c)
89	85, 88	sylibr 198	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) ⋀ S = ∪t) ⋀ (f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S))) → ran f ∈ ℘c)
90		domfi 4684	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((t ∈ Fin ⋀ ran f ≼ t) → ran f ∈ Fin)
91		simprr 415	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) → t ∈ Fin)
92	91	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) ⋀ S = ∪t) ⋀ (f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S))) → t ∈ Fin)
93		fodomfi 4709	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((t ∈ Fin ⋀ f:t–onto→ran f) → ran f ≼ t)
94		ffn 3734	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:t–→c → f Fn t)
95		dffn4 3785	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f Fn t ↔ f:t–onto→ran f)
96	94, 95	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f:t–→c → f:t–onto→ran f)
97	93, 96	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((t ∈ Fin ⋀ f:t–→c) → ran f ≼ t)
98	97	adantll 392	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin) ⋀ f:t–→c) → ran f ≼ t)
99	98	adantll 392	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) ⋀ f:t–→c) → ran f ≼ t)
100	99	ad2ant2r 409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) ⋀ S = ∪t) ⋀ (f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S))) → ran f ≼ t)
101	90, 92, 100	sylanc 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) ⋀ S = ∪t) ⋀ (f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S))) → ran f ∈ Fin)
102	89, 101	jca 286	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) ⋀ S = ∪t) ⋀ (f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S))) → (ran f ∈ ℘c ⋀ ran f ∈ Fin))
103		elin 2259	. . . . . . . . . . . . . . . . . . 19 ⊢ (ran f ∈ (℘c ∩ Fin) ↔ (ran f ∈ ℘c ⋀ ran f ∈ Fin))
104	102, 103	sylibr 198	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) ⋀ S = ∪t) ⋀ (f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S))) → ran f ∈ (℘c ∩ Fin))
105		pm2.27 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (u ∈ t → ((u ∈ t → u = ((f ‘u) ∩ S)) → u = ((f ‘u) ∩ S)))
106		inss1 2282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((f ‘u) ∩ S) ⊆ (f ‘u)
107		sseq1 2134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (u = ((f ‘u) ∩ S) → (u ⊆ (f ‘u) ↔ ((f ‘u) ∩ S) ⊆ (f ‘u)))
108	106, 107	mpbiri 192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (u = ((f ‘u) ∩ S) → u ⊆ (f ‘u))
109		ssel 2115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (u ⊆ (f ‘u) → (w ∈ u → w ∈ (f ‘u)))
110	109	a1dd 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (u ⊆ (f ‘u) → (w ∈ u → (f:t–→c → w ∈ (f ‘u))))
111	108, 110	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (u = ((f ‘u) ∩ S) → (w ∈ u → (f:t–→c → w ∈ (f ‘u))))
112	111	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (u ∈ t → (u = ((f ‘u) ∩ S) → (w ∈ u → (f:t–→c → w ∈ (f ‘u)))))
113	112	3imp 833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((u ∈ t ⋀ u = ((f ‘u) ∩ S) ⋀ w ∈ u) → (f:t–→c → w ∈ (f ‘u)))
114		fnfvelrn 3927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((f Fn t ⋀ u ∈ t) → (f ‘u) ∈ ran f)
115	114	expcom 372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (u ∈ t → (f Fn t → (f ‘u) ∈ ran f))
116	115	3ad2ant1 806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((u ∈ t ⋀ u = ((f ‘u) ∩ S) ⋀ w ∈ u) → (f Fn t → (f ‘u) ∈ ran f))
117	116, 94	syl5 21	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((u ∈ t ⋀ u = ((f ‘u) ∩ S) ⋀ w ∈ u) → (f:t–→c → (f ‘u) ∈ ran f))
118	113, 117	jcad 603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((u ∈ t ⋀ u = ((f ‘u) ∩ S) ⋀ w ∈ u) → (f:t–→c → (w ∈ (f ‘u) ⋀ (f ‘u) ∈ ran f)))
119	118	3exp 838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (u ∈ t → (u = ((f ‘u) ∩ S) → (w ∈ u → (f:t–→c → (w ∈ (f ‘u) ⋀ (f ‘u) ∈ ran f)))))
120	105, 119	syld 27	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (u ∈ t → ((u ∈ t → u = ((f ‘u) ∩ S)) → (w ∈ u → (f:t–→c → (w ∈ (f ‘u) ⋀ (f ‘u) ∈ ran f)))))
121	120	com3r 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (w ∈ u → (u ∈ t → ((u ∈ t → u = ((f ‘u) ∩ S)) → (f:t–→c → (w ∈ (f ‘u) ⋀ (f ‘u) ∈ ran f)))))
122	121	imp 348	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((w ∈ u ⋀ u ∈ t) → ((u ∈ t → u = ((f ‘u) ∩ S)) → (f:t–→c → (w ∈ (f ‘u) ⋀ (f ‘u) ∈ ran f))))
123	122	com3l 34	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((u ∈ t → u = ((f ‘u) ∩ S)) → (f:t–→c → ((w ∈ u ⋀ u ∈ t) → (w ∈ (f ‘u) ⋀ (f ‘u) ∈ ran f))))
124	123	impcom 349	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((f:t–→c ⋀ (u ∈ t → u = ((f ‘u) ∩ S))) → ((w ∈ u ⋀ u ∈ t) → (w ∈ (f ‘u) ⋀ (f ‘u) ∈ ran f)))
125		id 59	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (s = u → s = u)
126		fveq2 3835	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (s = u → (f ‘s) = (f ‘u))
127	126	ineq1d 2268	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (s = u → ((f ‘s) ∩ S) = ((f ‘u) ∩ S))
128	125, 127	eqeq12d 1532	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (s = u → (s = ((f ‘s) ∩ S) ↔ u = ((f ‘u) ∩ S)))
129	128	rcla4cv 1920	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀s ∈ t s = ((f ‘s) ∩ S) → (u ∈ t → u = ((f ‘u) ∩ S)))
130	124, 129	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S)) → ((w ∈ u ⋀ u ∈ t) → (w ∈ (f ‘u) ⋀ (f ‘u) ∈ ran f)))
131		fvex 3843	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f ‘u) ∈ V
132		eleq2 1578	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (v = (f ‘u) → (w ∈ v ↔ w ∈ (f ‘u)))
133		eleq1 1577	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (v = (f ‘u) → (v ∈ ran f ↔ (f ‘u) ∈ ran f))
134	132, 133	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (v = (f ‘u) → ((w ∈ v ⋀ v ∈ ran f) ↔ (w ∈ (f ‘u) ⋀ (f ‘u) ∈ ran f)))
135	131, 134	cla4ev 1915	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((w ∈ (f ‘u) ⋀ (f ‘u) ∈ ran f) → ∃v(w ∈ v ⋀ v ∈ ran f))
136	130, 135	syl6 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S)) → ((w ∈ u ⋀ u ∈ t) → ∃v(w ∈ v ⋀ v ∈ ran f)))
137	136	19.23adv 1251	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S)) → (∃u(w ∈ u ⋀ u ∈ t) → ∃v(w ∈ v ⋀ v ∈ ran f)))
138		eluni 2572	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (w ∈ ∪t ↔ ∃u(w ∈ u ⋀ u ∈ t))
139		eluni 2572	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (w ∈ ∪ran f ↔ ∃v(w ∈ v ⋀ v ∈ ran f))
140	137, 138, 139	3imtr4g 556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S)) → (w ∈ ∪t → w ∈ ∪ran f))
141	140	ssrdv 2122	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S)) → ∪t ⊆ ∪ran f)
142	141	adantl 388	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) ⋀ S = ∪t) ⋀ (f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S))) → ∪t ⊆ ∪ran f)
143		sseq1 2134	. . . . . . . . . . . . . . . . . . . 20 ⊢ (S = ∪t → (S ⊆ ∪ran f ↔ ∪t ⊆ ∪ran f))
144	143	ad2antlr 405	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) ⋀ S = ∪t) ⋀ (f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S))) → (S ⊆ ∪ran f ↔ ∪t ⊆ ∪ran f))
145	142, 144	mpbird 194	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) ⋀ S = ∪t) ⋀ (f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S))) → S ⊆ ∪ran f)
146	104, 145	jca 286	. . . . . . . . . . . . . . . . 17 ⊢ (((((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) ⋀ S = ∪t) ⋀ (f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S))) → (ran f ∈ (℘c ∩ Fin) ⋀ S ⊆ ∪ran f))
147	146	ex 371	. . . . . . . . . . . . . . . 16 ⊢ ((((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) ⋀ S = ∪t) → ((f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S)) → (ran f ∈ (℘c ∩ Fin) ⋀ S ⊆ ∪ran f)))
148	147	19.22dv 1328	. . . . . . . . . . . . . . 15 ⊢ ((((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) ⋀ S = ∪t) → (∃f(f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S)) → ∃f(ran f ∈ (℘c ∩ Fin) ⋀ S ⊆ ∪ran f)))
149	148	ex 371	. . . . . . . . . . . . . 14 ⊢ (((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) → (S = ∪t → (∃f(f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S)) → ∃f(ran f ∈ (℘c ∩ Fin) ⋀ S ⊆ ∪ran f))))
150	149	com23 32	. . . . . . . . . . . . 13 ⊢ (((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) → (∃f(f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S)) → (S = ∪t → ∃f(ran f ∈ (℘c ∩ Fin) ⋀ S ⊆ ∪ran f))))
151		unieq 2576	. . . . . . . . . . . . . . . 16 ⊢ (d = ran f → ∪d = ∪ran f)
152	151	sseq2d 2141	. . . . . . . . . . . . . . 15 ⊢ (d = ran f → (S ⊆ ∪d ↔ S ⊆ ∪ran f))
153	152	rcla4ev 1923	. . . . . . . . . . . . . 14 ⊢ ((ran f ∈ (℘c ∩ Fin) ⋀ S ⊆ ∪ran f) → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d)
154	153	19.23aiv 1333	. . . . . . . . . . . . 13 ⊢ (∃f(ran f ∈ (℘c ∩ Fin) ⋀ S ⊆ ∪ran f) → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d)
155	150, 154	syl8 24	. . . . . . . . . . . 12 ⊢ (((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) → (∃f(f:t–→c ⋀ ∀s ∈ t s = ((f ‘s) ∩ S)) → (S = ∪t → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d)))
156	83, 155	mpd 26	. . . . . . . . . . 11 ⊢ (((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin)) → (S = ∪t → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d))
157		elin 2259	. . . . . . . . . . . 12 ⊢ (t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin) ↔ (t ∈ ℘{x∣∃y ∈ c x = (y ∩ S)} ⋀ t ∈ Fin))
158	31	elpw 2461	. . . . . . . . . . . . . 14 ⊢ (t ∈ ℘{x∣∃y ∈ c x = (y ∩ S)} ↔ t ⊆ {x∣∃y ∈ c x = (y ∩ S)})
159		dfss3 2111	. . . . . . . . . . . . . 14 ⊢ (t ⊆ {x∣∃y ∈ c x = (y ∩ S)} ↔ ∀s ∈ t s ∈ {x∣∃y ∈ c x = (y ∩ S)})
160		visset 1859	. . . . . . . . . . . . . . . 16 ⊢ s ∈ V
161		eqeq1 1524	. . . . . . . . . . . . . . . . 17 ⊢ (x = s → (x = (y ∩ S) ↔ s = (y ∩ S)))
162	161	rexbidv 1710	. . . . . . . . . . . . . . . 16 ⊢ (x = s → (∃y ∈ c x = (y ∩ S) ↔ ∃y ∈ c s = (y ∩ S)))
163	160, 162	elab 1943	. . . . . . . . . . . . . . 15 ⊢ (s ∈ {x∣∃y ∈ c x = (y ∩ S)} ↔ ∃y ∈ c s = (y ∩ S))
164	163	ralbii 1713	. . . . . . . . . . . . . 14 ⊢ (∀s ∈ t s ∈ {x∣∃y ∈ c x = (y ∩ S)} ↔ ∀s ∈ t ∃y ∈ c s = (y ∩ S))
165	158, 159, 164	3bitri 175	. . . . . . . . . . . . 13 ⊢ (t ∈ ℘{x∣∃y ∈ c x = (y ∩ S)} ↔ ∀s ∈ t ∃y ∈ c s = (y ∩ S))
166	165	anbi1i 484	. . . . . . . . . . . 12 ⊢ ((t ∈ ℘{x∣∃y ∈ c x = (y ∩ S)} ⋀ t ∈ Fin) ↔ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin))
167	157, 166	bitri 171	. . . . . . . . . . 11 ⊢ (t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin) ↔ (∀s ∈ t ∃y ∈ c s = (y ∩ S) ⋀ t ∈ Fin))
168	156, 167	sylan2b 454	. . . . . . . . . 10 ⊢ (((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) ⋀ t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)) → (S = ∪t → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d))
169	168	r19.23adva 1793	. . . . . . . . 9 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → (∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)S = ∪t → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d))
170		eqid 1518	. . . . . . . . . 10 ⊢ S = S
171	170	a1bi 195	. . . . . . . . 9 ⊢ (∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)S = ∪t ↔ (S = S → ∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)S = ∪t))
172	169, 171	syl5ibr 205	. . . . . . . 8 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → ((S = S → ∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)S = ∪t) → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d))
173	78, 172	sylbid 201	. . . . . . 7 ⊢ ((((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) ⋀ S ⊆ ∪c) → ((∪(subSp ‘S, J) = ∪{x∣∃y ∈ c x = (y ∩ S)} → ∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)∪(subSp ‘S, J) = ∪t) → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d))
174	173	ex 371	. . . . . 6 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) → (S ⊆ ∪c → ((∪(subSp ‘S, J) = ∪{x∣∃y ∈ c x = (y ∩ S)} → ∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)∪(subSp ‘S, J) = ∪t) → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d)))
175	174	com23 32	. . . . 5 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) → ((∪(subSp ‘S, J) = ∪{x∣∃y ∈ c x = (y ∩ S)} → ∃t ∈ (℘{x∣∃y ∈ c x = (y ∩ S)} ∩ Fin)∪(subSp ‘S, J) = ∪t) → (S ⊆ ∪c → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d)))
176	50, 175	syld 27	. . . 4 ⊢ (((J ∈ Top ⋀ S ⊆ X) ⋀ c ∈ ℘J) → (∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t) → (S ⊆ ∪c → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d)))
177	176	r19.21adva 1765	. . 3 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t) → ∀c ∈ ℘ J(S ⊆ ∪c → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d)))
178	2	compsublem 11480	. . 3 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (∀c ∈ ℘ J(S ⊆ ∪c → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d) → ∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t)))
179	177, 178	impbid 519	. 2 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (∀s ∈ ℘ (subSp ‘S, J)(∪(subSp ‘S, J) = ∪s → ∃t ∈ (℘s ∩ Fin)∪(subSp ‘S, J) = ∪t) ↔ ∀c ∈ ℘ J(S ⊆ ∪c → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d)))
180	9, 179	bitrd 531	1 ⊢ ((J ∈ Top ⋀ S ⊆ X) → ((subSp ‘S, J) ∈ Comp ↔ ∀c ∈ ℘ J(S ⊆ ∪c → ∃d ∈ (℘c ∩ Fin)S ⊆ ∪d)))

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 144 ⋀ wa 221 ⋀ w3a 781 = wceq 992 ∈ wcel 994 ∃wex 1016 {cab 1505 ∀wral 1691 ∃wrex 1692 Vcvv 1857 ∩ cin 2098 ⊆ wss 2099 ℘cpw 2458

cop 2469 ∪cuni 2569 ∪ciun 2633 class class class wbr 2692 ran crn 3252 Fn wfn 3258 –→wf 3259 –onto→wfo 3261 ‘cfv 3263 ≼ cdom 4506 Fincfn 4508 Topctop 7800 subSpcsubsp 11045 Compccomp 11105

This theorem is referenced by: cptclsscpt 11482 uncomp 11483 hscptsscld 11484

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 ax-reg 4736

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-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-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-1o 4269 df-er 4401 df-en 4509 df-dom 4510 df-fin 4512 df-top 7804 df-topsp 7805 df-subsp 11046 df-comp 11106