Metamath Proof Explorer


Theorem cmpcld

Description: A closed subset of a compact space is compact. (Contributed by Jeff Hankins, 29-Jun-2009)

Ref Expression
Assertion cmpcld ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽t 𝑆 ) ∈ Comp )

Proof

Step Hyp Ref Expression
1 velpw ( 𝑠 ∈ 𝒫 𝐽𝑠𝐽 )
2 simp1l ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → 𝐽 ∈ Comp )
3 simp2 ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → 𝑠𝐽 )
4 eqid 𝐽 = 𝐽
5 4 cldopn ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → ( 𝐽𝑆 ) ∈ 𝐽 )
6 5 adantl ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽𝑆 ) ∈ 𝐽 )
7 6 3ad2ant1 ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → ( 𝐽𝑆 ) ∈ 𝐽 )
8 7 snssd ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → { ( 𝐽𝑆 ) } ⊆ 𝐽 )
9 3 8 unssd ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ⊆ 𝐽 )
10 simp3 ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → 𝑆 𝑠 )
11 uniss ( 𝑠𝐽 𝑠 𝐽 )
12 11 3ad2ant2 ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → 𝑠 𝐽 )
13 10 12 sstrd ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → 𝑆 𝐽 )
14 undif ( 𝑆 𝐽 ↔ ( 𝑆 ∪ ( 𝐽𝑆 ) ) = 𝐽 )
15 13 14 sylib ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → ( 𝑆 ∪ ( 𝐽𝑆 ) ) = 𝐽 )
16 unss1 ( 𝑆 𝑠 → ( 𝑆 ∪ ( 𝐽𝑆 ) ) ⊆ ( 𝑠 ∪ ( 𝐽𝑆 ) ) )
17 16 3ad2ant3 ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → ( 𝑆 ∪ ( 𝐽𝑆 ) ) ⊆ ( 𝑠 ∪ ( 𝐽𝑆 ) ) )
18 15 17 eqsstrrd ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → 𝐽 ⊆ ( 𝑠 ∪ ( 𝐽𝑆 ) ) )
19 difss ( 𝐽𝑆 ) ⊆ 𝐽
20 unss ( ( 𝑠 𝐽 ∧ ( 𝐽𝑆 ) ⊆ 𝐽 ) ↔ ( 𝑠 ∪ ( 𝐽𝑆 ) ) ⊆ 𝐽 )
21 12 19 20 sylanblc ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → ( 𝑠 ∪ ( 𝐽𝑆 ) ) ⊆ 𝐽 )
22 18 21 eqssd ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → 𝐽 = ( 𝑠 ∪ ( 𝐽𝑆 ) ) )
23 uniexg ( 𝐽 ∈ Comp → 𝐽 ∈ V )
24 23 ad2antrr ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽 ) → 𝐽 ∈ V )
25 24 3adant3 ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → 𝐽 ∈ V )
26 difexg ( 𝐽 ∈ V → ( 𝐽𝑆 ) ∈ V )
27 unisng ( ( 𝐽𝑆 ) ∈ V → { ( 𝐽𝑆 ) } = ( 𝐽𝑆 ) )
28 25 26 27 3syl ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → { ( 𝐽𝑆 ) } = ( 𝐽𝑆 ) )
29 28 uneq2d ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → ( 𝑠 { ( 𝐽𝑆 ) } ) = ( 𝑠 ∪ ( 𝐽𝑆 ) ) )
30 22 29 eqtr4d ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → 𝐽 = ( 𝑠 { ( 𝐽𝑆 ) } ) )
31 uniun ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) = ( 𝑠 { ( 𝐽𝑆 ) } )
32 30 31 eqtr4di ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → 𝐽 = ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) )
33 4 cmpcov ( ( 𝐽 ∈ Comp ∧ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ⊆ 𝐽 𝐽 = ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ) → ∃ 𝑢 ∈ ( 𝒫 ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∩ Fin ) 𝐽 = 𝑢 )
34 2 9 32 33 syl3anc ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → ∃ 𝑢 ∈ ( 𝒫 ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∩ Fin ) 𝐽 = 𝑢 )
35 elfpw ( 𝑢 ∈ ( 𝒫 ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∩ Fin ) ↔ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) )
36 simp2l ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) → 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) )
37 uncom ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) = ( { ( 𝐽𝑆 ) } ∪ 𝑠 )
38 36 37 sseqtrdi ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) → 𝑢 ⊆ ( { ( 𝐽𝑆 ) } ∪ 𝑠 ) )
39 ssundif ( 𝑢 ⊆ ( { ( 𝐽𝑆 ) } ∪ 𝑠 ) ↔ ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ⊆ 𝑠 )
40 38 39 sylib ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) → ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ⊆ 𝑠 )
41 diffi ( 𝑢 ∈ Fin → ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ∈ Fin )
42 41 ad2antll ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ) → ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ∈ Fin )
43 42 3adant3 ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) → ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ∈ Fin )
44 elfpw ( ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ∈ ( 𝒫 𝑠 ∩ Fin ) ↔ ( ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ⊆ 𝑠 ∧ ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ∈ Fin ) )
45 40 43 44 sylanbrc ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) → ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ∈ ( 𝒫 𝑠 ∩ Fin ) )
46 10 3ad2ant1 ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) → 𝑆 𝑠 )
47 12 3ad2ant1 ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) → 𝑠 𝐽 )
48 simp3 ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) → 𝐽 = 𝑢 )
49 47 48 sseqtrd ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) → 𝑠 𝑢 )
50 46 49 sstrd ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) → 𝑆 𝑢 )
51 50 sselda ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) → 𝑣 𝑢 )
52 eluni ( 𝑣 𝑢 ↔ ∃ 𝑤 ( 𝑣𝑤𝑤𝑢 ) )
53 51 52 sylib ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) → ∃ 𝑤 ( 𝑣𝑤𝑤𝑢 ) )
54 simpl ( ( 𝑣𝑤𝑤𝑢 ) → 𝑣𝑤 )
55 54 a1i ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) → ( ( 𝑣𝑤𝑤𝑢 ) → 𝑣𝑤 ) )
56 simpr ( ( 𝑣𝑤𝑤𝑢 ) → 𝑤𝑢 )
57 56 a1i ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) → ( ( 𝑣𝑤𝑤𝑢 ) → 𝑤𝑢 ) )
58 elndif ( 𝑣𝑆 → ¬ 𝑣 ∈ ( 𝐽𝑆 ) )
59 58 ad2antlr ( ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) ∧ 𝑣𝑤 ) → ¬ 𝑣 ∈ ( 𝐽𝑆 ) )
60 eleq2 ( 𝑤 = ( 𝐽𝑆 ) → ( 𝑣𝑤𝑣 ∈ ( 𝐽𝑆 ) ) )
61 60 biimpd ( 𝑤 = ( 𝐽𝑆 ) → ( 𝑣𝑤𝑣 ∈ ( 𝐽𝑆 ) ) )
62 61 a1i ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) → ( 𝑤 = ( 𝐽𝑆 ) → ( 𝑣𝑤𝑣 ∈ ( 𝐽𝑆 ) ) ) )
63 62 com23 ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) → ( 𝑣𝑤 → ( 𝑤 = ( 𝐽𝑆 ) → 𝑣 ∈ ( 𝐽𝑆 ) ) ) )
64 63 imp ( ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) ∧ 𝑣𝑤 ) → ( 𝑤 = ( 𝐽𝑆 ) → 𝑣 ∈ ( 𝐽𝑆 ) ) )
65 59 64 mtod ( ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) ∧ 𝑣𝑤 ) → ¬ 𝑤 = ( 𝐽𝑆 ) )
66 65 ex ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) → ( 𝑣𝑤 → ¬ 𝑤 = ( 𝐽𝑆 ) ) )
67 66 adantrd ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) → ( ( 𝑣𝑤𝑤𝑢 ) → ¬ 𝑤 = ( 𝐽𝑆 ) ) )
68 velsn ( 𝑤 ∈ { ( 𝐽𝑆 ) } ↔ 𝑤 = ( 𝐽𝑆 ) )
69 68 notbii ( ¬ 𝑤 ∈ { ( 𝐽𝑆 ) } ↔ ¬ 𝑤 = ( 𝐽𝑆 ) )
70 67 69 syl6ibr ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) → ( ( 𝑣𝑤𝑤𝑢 ) → ¬ 𝑤 ∈ { ( 𝐽𝑆 ) } ) )
71 57 70 jcad ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) → ( ( 𝑣𝑤𝑤𝑢 ) → ( 𝑤𝑢 ∧ ¬ 𝑤 ∈ { ( 𝐽𝑆 ) } ) ) )
72 eldif ( 𝑤 ∈ ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ↔ ( 𝑤𝑢 ∧ ¬ 𝑤 ∈ { ( 𝐽𝑆 ) } ) )
73 71 72 syl6ibr ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) → ( ( 𝑣𝑤𝑤𝑢 ) → 𝑤 ∈ ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ) )
74 55 73 jcad ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) → ( ( 𝑣𝑤𝑤𝑢 ) → ( 𝑣𝑤𝑤 ∈ ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ) ) )
75 74 eximdv ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) → ( ∃ 𝑤 ( 𝑣𝑤𝑤𝑢 ) → ∃ 𝑤 ( 𝑣𝑤𝑤 ∈ ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ) ) )
76 53 75 mpd ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) ∧ 𝑣𝑆 ) → ∃ 𝑤 ( 𝑣𝑤𝑤 ∈ ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ) )
77 76 ex ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) → ( 𝑣𝑆 → ∃ 𝑤 ( 𝑣𝑤𝑤 ∈ ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ) ) )
78 eluni ( 𝑣 ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ↔ ∃ 𝑤 ( 𝑣𝑤𝑤 ∈ ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ) )
79 77 78 syl6ibr ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) → ( 𝑣𝑆𝑣 ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ) )
80 79 ssrdv ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) → 𝑆 ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) )
81 unieq ( 𝑡 = ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) → 𝑡 = ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) )
82 81 sseq2d ( 𝑡 = ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) → ( 𝑆 𝑡𝑆 ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ) )
83 82 rspcev ( ( ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ∈ ( 𝒫 𝑠 ∩ Fin ) ∧ 𝑆 ( 𝑢 ∖ { ( 𝐽𝑆 ) } ) ) → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) 𝑆 𝑡 )
84 45 80 83 syl2anc ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ 𝐽 = 𝑢 ) → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) 𝑆 𝑡 )
85 35 84 syl3an2b ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) ∧ 𝑢 ∈ ( 𝒫 ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∩ Fin ) ∧ 𝐽 = 𝑢 ) → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) 𝑆 𝑡 )
86 85 rexlimdv3a ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → ( ∃ 𝑢 ∈ ( 𝒫 ( 𝑠 ∪ { ( 𝐽𝑆 ) } ) ∩ Fin ) 𝐽 = 𝑢 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) 𝑆 𝑡 ) )
87 34 86 mpd ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠𝐽𝑆 𝑠 ) → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) 𝑆 𝑡 )
88 87 3exp ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑠𝐽 → ( 𝑆 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) 𝑆 𝑡 ) ) )
89 1 88 syl5bi ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑠 ∈ 𝒫 𝐽 → ( 𝑆 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) 𝑆 𝑡 ) ) )
90 89 ralrimiv ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ∀ 𝑠 ∈ 𝒫 𝐽 ( 𝑆 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) 𝑆 𝑡 ) )
91 cmptop ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
92 4 cldss ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → 𝑆 𝐽 )
93 4 cmpsub ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) → ( ( 𝐽t 𝑆 ) ∈ Comp ↔ ∀ 𝑠 ∈ 𝒫 𝐽 ( 𝑆 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) 𝑆 𝑡 ) ) )
94 91 92 93 syl2an ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝐽t 𝑆 ) ∈ Comp ↔ ∀ 𝑠 ∈ 𝒫 𝐽 ( 𝑆 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) 𝑆 𝑡 ) ) )
95 90 94 mpbird ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽t 𝑆 ) ∈ Comp )