Theorem cptclsscpt 11482

Description: A closed subset of a compact space is compact.

Assertion

Ref	Expression
cptclsscpt	⊢ ((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) → (subSp ‘<.S, J>.) ∈ Comp)

Proof of Theorem cptclsscpt

Step	Hyp	Ref	Expression
1		eqid 1518	. . . . . . . 8 ⊢ ∪J = ∪J
2	1	compcov 11479	. . . . . . 7 ⊢ ((J ∈ Comp ⋀ (s ∪ {(∪J ∖ S)}) ⊆ J ⋀ ∪J = ∪(s ∪ {(∪J ∖ S)})) → ∃u ∈ (℘(s ∪ {(∪J ∖ S)}) ∩ Fin)∪J = ∪u)
3		simpll 412	. . . . . . . 8 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J) → J ∈ Comp)
4	3	3adant3 805	. . . . . . 7 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → J ∈ Comp)
5		3simp2 795	. . . . . . . . 9 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → s ⊆ J)
6	1	cldopn 7882	. . . . . . . . . . . 12 ⊢ ((J ∈ Top ⋀ S ∈ (Clsd ‘J)) → (∪J ∖ S) ∈ J)
7		comptop 11478	. . . . . . . . . . . 12 ⊢ (J ∈ Comp → J ∈ Top)
8	6, 7	sylan 450	. . . . . . . . . . 11 ⊢ ((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) → (∪J ∖ S) ∈ J)
9	8	3ad2ant1 806	. . . . . . . . . 10 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → (∪J ∖ S) ∈ J)
10		snssi 2530	. . . . . . . . . 10 ⊢ ((∪J ∖ S) ∈ J → {(∪J ∖ S)} ⊆ J)
11	9, 10	syl 10	. . . . . . . . 9 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → {(∪J ∖ S)} ⊆ J)
12	5, 11	jca 286	. . . . . . . 8 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → (s ⊆ J ⋀ {(∪J ∖ S)} ⊆ J))
13		unss 2256	. . . . . . . 8 ⊢ ((s ⊆ J ⋀ {(∪J ∖ S)} ⊆ J) ↔ (s ∪ {(∪J ∖ S)}) ⊆ J)
14	12, 13	sylib 196	. . . . . . 7 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → (s ∪ {(∪J ∖ S)}) ⊆ J)
15		3simp3 796	. . . . . . . . . . . . 13 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → S ⊆ ∪s)
16		uniss 2588	. . . . . . . . . . . . . 14 ⊢ (s ⊆ J → ∪s ⊆ ∪J)
17	16	3ad2ant2 807	. . . . . . . . . . . . 13 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → ∪s ⊆ ∪J)
18	15, 17	sstrd 2126	. . . . . . . . . . . 12 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → S ⊆ ∪J)
19		undif 2397	. . . . . . . . . . . 12 ⊢ (S ⊆ ∪J ↔ (S ∪ (∪J ∖ S)) = ∪J)
20	18, 19	sylib 196	. . . . . . . . . . 11 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → (S ∪ (∪J ∖ S)) = ∪J)
21		unss1 2251	. . . . . . . . . . . 12 ⊢ (S ⊆ ∪s → (S ∪ (∪J ∖ S)) ⊆ (∪s ∪ (∪J ∖ S)))
22	21	3ad2ant3 808	. . . . . . . . . . 11 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → (S ∪ (∪J ∖ S)) ⊆ (∪s ∪ (∪J ∖ S)))
23	20, 22	eqsstr3d 2148	. . . . . . . . . 10 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → ∪J ⊆ (∪s ∪ (∪J ∖ S)))
24		difss 2219	. . . . . . . . . . . 12 ⊢ (∪J ∖ S) ⊆ ∪J
25	17, 24	jctir 291	. . . . . . . . . . 11 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → (∪s ⊆ ∪J ⋀ (∪J ∖ S) ⊆ ∪J))
26		unss 2256	. . . . . . . . . . 11 ⊢ ((∪s ⊆ ∪J ⋀ (∪J ∖ S) ⊆ ∪J) ↔ (∪s ∪ (∪J ∖ S)) ⊆ ∪J)
27	25, 26	sylib 196	. . . . . . . . . 10 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → (∪s ∪ (∪J ∖ S)) ⊆ ∪J)
28	23, 27	eqssd 2131	. . . . . . . . 9 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → ∪J = (∪s ∪ (∪J ∖ S)))
29		uniexg 3094	. . . . . . . . . . . . 13 ⊢ (J ∈ Comp → ∪J ∈ V)
30	29	ad2antrr 404	. . . . . . . . . . . 12 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J) → ∪J ∈ V)
31	30	3adant3 805	. . . . . . . . . . 11 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → ∪J ∈ V)
32		difexg 2796	. . . . . . . . . . 11 ⊢ (∪J ∈ V → (∪J ∖ S) ∈ V)
33		unisng 2585	. . . . . . . . . . 11 ⊢ ((∪J ∖ S) ∈ V → ∪{(∪J ∖ S)} = (∪J ∖ S))
34	31, 32, 33	3syl 20	. . . . . . . . . 10 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → ∪{(∪J ∖ S)} = (∪J ∖ S))
35	34	uneq2d 2236	. . . . . . . . 9 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → (∪s ∪ ∪{(∪J ∖ S)}) = (∪s ∪ (∪J ∖ S)))
36	28, 35	eqtr4d 1553	. . . . . . . 8 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → ∪J = (∪s ∪ ∪{(∪J ∖ S)}))
37		uniun 2586	. . . . . . . 8 ⊢ ∪(s ∪ {(∪J ∖ S)}) = (∪s ∪ ∪{(∪J ∖ S)})
38	36, 37	syl6eqr 1568	. . . . . . 7 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → ∪J = ∪(s ∪ {(∪J ∖ S)}))
39	2, 4, 14, 38	syl3anc 864	. . . . . 6 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → ∃u ∈ (℘(s ∪ {(∪J ∖ S)}) ∩ Fin)∪J = ∪u)
40		unieq 2576	. . . . . . . . . . . 12 ⊢ (t = (u ∖ {(∪J ∖ S)}) → ∪t = ∪(u ∖ {(∪J ∖ S)}))
41	40	sseq2d 2141	. . . . . . . . . . 11 ⊢ (t = (u ∖ {(∪J ∖ S)}) → (S ⊆ ∪t ↔ S ⊆ ∪(u ∖ {(∪J ∖ S)})))
42	41	rcla4ev 1923	. . . . . . . . . 10 ⊢ (((u ∖ {(∪J ∖ S)}) ∈ (℘s ∩ Fin) ⋀ S ⊆ ∪(u ∖ {(∪J ∖ S)})) → ∃t ∈ (℘s ∩ Fin)S ⊆ ∪t)
43		simprl 414	. . . . . . . . . . . . . . 15 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin)) → u ⊆ (s ∪ {(∪J ∖ S)}))
44	43	3adant3 805	. . . . . . . . . . . . . 14 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → u ⊆ (s ∪ {(∪J ∖ S)}))
45		uncom 2228	. . . . . . . . . . . . . 14 ⊢ (s ∪ {(∪J ∖ S)}) = ({(∪J ∖ S)} ∪ s)
46	44, 45	syl6ss 2159	. . . . . . . . . . . . 13 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → u ⊆ ({(∪J ∖ S)} ∪ s))
47		ssundif 2398	. . . . . . . . . . . . 13 ⊢ (u ⊆ ({(∪J ∖ S)} ∪ s) ↔ (u ∖ {(∪J ∖ S)}) ⊆ s)
48	46, 47	sylib 196	. . . . . . . . . . . 12 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → (u ∖ {(∪J ∖ S)}) ⊆ s)
49		difss 2219	. . . . . . . . . . . . . . 15 ⊢ (u ∖ {(∪J ∖ S)}) ⊆ u
50		ssfi 4683	. . . . . . . . . . . . . . 15 ⊢ ((u ∈ Fin ⋀ (u ∖ {(∪J ∖ S)}) ⊆ u) → (u ∖ {(∪J ∖ S)}) ∈ Fin)
51	49, 50	mpan2 700	. . . . . . . . . . . . . 14 ⊢ (u ∈ Fin → (u ∖ {(∪J ∖ S)}) ∈ Fin)
52	51	ad2antll 407	. . . . . . . . . . . . 13 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin)) → (u ∖ {(∪J ∖ S)}) ∈ Fin)
53	52	3adant3 805	. . . . . . . . . . . 12 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → (u ∖ {(∪J ∖ S)}) ∈ Fin)
54	48, 53	jca 286	. . . . . . . . . . 11 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → ((u ∖ {(∪J ∖ S)}) ⊆ s ⋀ (u ∖ {(∪J ∖ S)}) ∈ Fin))
55		elin 2259	. . . . . . . . . . . 12 ⊢ ((u ∖ {(∪J ∖ S)}) ∈ (℘s ∩ Fin) ↔ ((u ∖ {(∪J ∖ S)}) ∈ ℘s ⋀ (u ∖ {(∪J ∖ S)}) ∈ Fin))
56		visset 1859	. . . . . . . . . . . . . . 15 ⊢ u ∈ V
57	56, 49	ssexi 2794	. . . . . . . . . . . . . 14 ⊢ (u ∖ {(∪J ∖ S)}) ∈ V
58	57	elpw 2461	. . . . . . . . . . . . 13 ⊢ ((u ∖ {(∪J ∖ S)}) ∈ ℘s ↔ (u ∖ {(∪J ∖ S)}) ⊆ s)
59	58	anbi1i 484	. . . . . . . . . . . 12 ⊢ (((u ∖ {(∪J ∖ S)}) ∈ ℘s ⋀ (u ∖ {(∪J ∖ S)}) ∈ Fin) ↔ ((u ∖ {(∪J ∖ S)}) ⊆ s ⋀ (u ∖ {(∪J ∖ S)}) ∈ Fin))
60	55, 59	bitri 171	. . . . . . . . . . 11 ⊢ ((u ∖ {(∪J ∖ S)}) ∈ (℘s ∩ Fin) ↔ ((u ∖ {(∪J ∖ S)}) ⊆ s ⋀ (u ∖ {(∪J ∖ S)}) ∈ Fin))
61	54, 60	sylibr 198	. . . . . . . . . 10 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → (u ∖ {(∪J ∖ S)}) ∈ (℘s ∩ Fin))
62	15	3ad2ant1 806	. . . . . . . . . . . . . . . . . 18 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → S ⊆ ∪s)
63	17	3ad2ant1 806	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → ∪s ⊆ ∪J)
64		3simp3 796	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → ∪J = ∪u)
65	63, 64	sseqtrd 2149	. . . . . . . . . . . . . . . . . 18 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → ∪s ⊆ ∪u)
66	62, 65	sstrd 2126	. . . . . . . . . . . . . . . . 17 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → S ⊆ ∪u)
67	66	sseld 2119	. . . . . . . . . . . . . . . 16 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → (v ∈ S → v ∈ ∪u))
68	67	imp 348	. . . . . . . . . . . . . . 15 ⊢ (((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) → v ∈ ∪u)
69		eluni 2572	. . . . . . . . . . . . . . 15 ⊢ (v ∈ ∪u ↔ ∃w(v ∈ w ⋀ w ∈ u))
70	68, 69	sylib 196	. . . . . . . . . . . . . 14 ⊢ (((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) → ∃w(v ∈ w ⋀ w ∈ u))
71		pm3.26 317	. . . . . . . . . . . . . . . . 17 ⊢ ((v ∈ w ⋀ w ∈ u) → v ∈ w)
72	71	a1i 8	. . . . . . . . . . . . . . . 16 ⊢ (((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) → ((v ∈ w ⋀ w ∈ u) → v ∈ w))
73		pm3.27 321	. . . . . . . . . . . . . . . . . . 19 ⊢ ((v ∈ w ⋀ w ∈ u) → w ∈ u)
74	73	a1i 8	. . . . . . . . . . . . . . . . . 18 ⊢ (((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) → ((v ∈ w ⋀ w ∈ u) → w ∈ u))
75		elndif 2216	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (v ∈ S → ¬ v ∈ (∪J ∖ S))
76	75	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) ⋀ v ∈ w) → ¬ v ∈ (∪J ∖ S))
77		eleq2 1578	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (w = (∪J ∖ S) → (v ∈ w ↔ v ∈ (∪J ∖ S)))
78	77	biimpd 151	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (w = (∪J ∖ S) → (v ∈ w → v ∈ (∪J ∖ S)))
79	78	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) → (w = (∪J ∖ S) → (v ∈ w → v ∈ (∪J ∖ S))))
80	79	com23 32	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) → (v ∈ w → (w = (∪J ∖ S) → v ∈ (∪J ∖ S))))
81	80	imp 348	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) ⋀ v ∈ w) → (w = (∪J ∖ S) → v ∈ (∪J ∖ S)))
82	76, 81	mtod 107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) ⋀ v ∈ w) → ¬ w = (∪J ∖ S))
83	82	ex 371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) → (v ∈ w → ¬ w = (∪J ∖ S)))
84	83	adantrd 391	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) → ((v ∈ w ⋀ w ∈ u) → ¬ w = (∪J ∖ S)))
85		elsn 2479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (w ∈ {(∪J ∖ S)} ↔ w = (∪J ∖ S))
86	85	notbii 185	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ w ∈ {(∪J ∖ S)} ↔ ¬ w = (∪J ∖ S))
87	84, 86	syl6ibr 211	. . . . . . . . . . . . . . . . . 18 ⊢ (((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) → ((v ∈ w ⋀ w ∈ u) → ¬ w ∈ {(∪J ∖ S)}))
88	74, 87	jcad 603	. . . . . . . . . . . . . . . . 17 ⊢ (((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) → ((v ∈ w ⋀ w ∈ u) → (w ∈ u ⋀ ¬ w ∈ {(∪J ∖ S)})))
89		eldif 2109	. . . . . . . . . . . . . . . . 17 ⊢ (w ∈ (u ∖ {(∪J ∖ S)}) ↔ (w ∈ u ⋀ ¬ w ∈ {(∪J ∖ S)}))
90	88, 89	syl6ibr 211	. . . . . . . . . . . . . . . 16 ⊢ (((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) → ((v ∈ w ⋀ w ∈ u) → w ∈ (u ∖ {(∪J ∖ S)})))
91	72, 90	jcad 603	. . . . . . . . . . . . . . 15 ⊢ (((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) → ((v ∈ w ⋀ w ∈ u) → (v ∈ w ⋀ w ∈ (u ∖ {(∪J ∖ S)}))))
92	91	19.22dv 1328	. . . . . . . . . . . . . 14 ⊢ (((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) → (∃w(v ∈ w ⋀ w ∈ u) → ∃w(v ∈ w ⋀ w ∈ (u ∖ {(∪J ∖ S)}))))
93	70, 92	mpd 26	. . . . . . . . . . . . 13 ⊢ (((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) ⋀ v ∈ S) → ∃w(v ∈ w ⋀ w ∈ (u ∖ {(∪J ∖ S)})))
94	93	ex 371	. . . . . . . . . . . 12 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → (v ∈ S → ∃w(v ∈ w ⋀ w ∈ (u ∖ {(∪J ∖ S)}))))
95		eluni 2572	. . . . . . . . . . . 12 ⊢ (v ∈ ∪(u ∖ {(∪J ∖ S)}) ↔ ∃w(v ∈ w ⋀ w ∈ (u ∖ {(∪J ∖ S)})))
96	94, 95	syl6ibr 211	. . . . . . . . . . 11 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → (v ∈ S → v ∈ ∪(u ∖ {(∪J ∖ S)})))
97	96	ssrdv 2122	. . . . . . . . . 10 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → S ⊆ ∪(u ∖ {(∪J ∖ S)}))
98	42, 61, 97	sylanc 473	. . . . . . . . 9 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ⋀ ∪J = ∪u) → ∃t ∈ (℘s ∩ Fin)S ⊆ ∪t)
99		elin 2259	. . . . . . . . . 10 ⊢ (u ∈ (℘(s ∪ {(∪J ∖ S)}) ∩ Fin) ↔ (u ∈ ℘(s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin))
100	56	elpw 2461	. . . . . . . . . . 11 ⊢ (u ∈ ℘(s ∪ {(∪J ∖ S)}) ↔ u ⊆ (s ∪ {(∪J ∖ S)}))
101	100	anbi1i 484	. . . . . . . . . 10 ⊢ ((u ∈ ℘(s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin) ↔ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin))
102	99, 101	bitri 171	. . . . . . . . 9 ⊢ (u ∈ (℘(s ∪ {(∪J ∖ S)}) ∩ Fin) ↔ (u ⊆ (s ∪ {(∪J ∖ S)}) ⋀ u ∈ Fin))
103	98, 102	syl3an2b 869	. . . . . . . 8 ⊢ ((((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) ⋀ u ∈ (℘(s ∪ {(∪J ∖ S)}) ∩ Fin) ⋀ ∪J = ∪u) → ∃t ∈ (℘s ∩ Fin)S ⊆ ∪t)
104	103	3exp 838	. . . . . . 7 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → (u ∈ (℘(s ∪ {(∪J ∖ S)}) ∩ Fin) → (∪J = ∪u → ∃t ∈ (℘s ∩ Fin)S ⊆ ∪t)))
105	104	r19.23adv 1792	. . . . . 6 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → (∃u ∈ (℘(s ∪ {(∪J ∖ S)}) ∩ Fin)∪J = ∪u → ∃t ∈ (℘s ∩ Fin)S ⊆ ∪t))
106	39, 105	mpd 26	. . . . 5 ⊢ (((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) ⋀ s ⊆ J ⋀ S ⊆ ∪s) → ∃t ∈ (℘s ∩ Fin)S ⊆ ∪t)
107	106	3exp 838	. . . 4 ⊢ ((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) → (s ⊆ J → (S ⊆ ∪s → ∃t ∈ (℘s ∩ Fin)S ⊆ ∪t)))
108		visset 1859	. . . . 5 ⊢ s ∈ V
109	108	elpw 2461	. . . 4 ⊢ (s ∈ ℘J ↔ s ⊆ J)
110	107, 109	syl5ib 204	. . 3 ⊢ ((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) → (s ∈ ℘J → (S ⊆ ∪s → ∃t ∈ (℘s ∩ Fin)S ⊆ ∪t)))
111	110	r19.21aiv 1759	. 2 ⊢ ((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) → ∀s ∈ ℘ J(S ⊆ ∪s → ∃t ∈ (℘s ∩ Fin)S ⊆ ∪t))
112	1	cldss 7881	. . . 4 ⊢ ((J ∈ Top ⋀ S ∈ (Clsd ‘J)) → S ⊆ ∪J)
113	1	compsub 11481	. . . 4 ⊢ ((J ∈ Top ⋀ S ⊆ ∪J) → ((subSp ‘<.S, J>.) ∈ Comp ↔ ∀s ∈ ℘ J(S ⊆ ∪s → ∃t ∈ (℘s ∩ Fin)S ⊆ ∪t)))
114	112, 113	syldan 469	. . 3 ⊢ ((J ∈ Top ⋀ S ∈ (Clsd ‘J)) → ((subSp ‘<.S, J>.) ∈ Comp ↔ ∀s ∈ ℘ J(S ⊆ ∪s → ∃t ∈ (℘s ∩ Fin)S ⊆ ∪t)))
115	114, 7	sylan 450	. 2 ⊢ ((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) → ((subSp ‘<.S, J>.) ∈ Comp ↔ ∀s ∈ ℘ J(S ⊆ ∪s → ∃t ∈ (℘s ∩ Fin)S ⊆ ∪t)))
116	111, 115	mpbird 194	1 ⊢ ((J ∈ Comp ⋀ S ∈ (Clsd ‘J)) → (subSp ‘<.S, J>.) ∈ Comp)

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 144   ⋀ wa 221   ⋀ w3a 781   = wceq 992   ∈ wcel 994  ∃wex 1016  ∀wral 1691  ∃wrex 1692  Vcvv 1857   ∖ cdif 2096   ∪ cun 2097   ∩ cin 2098   ⊆ wss 2099  ℘cpw 2458  {csn 2467  <.cop 2469  ∪cuni 2569   ‘cfv 3263  Fincfn 4508  Topctop 7800  Clsdccld 7870  subSpcsubsp 11045  Compccomp 11105

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-cld 7873  df-subsp 11046  df-comp 11106

Copyright terms: Public domain