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 imbitrrdi ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( ∪ 𝐽 ∖ 𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑢 ) ∧ 𝑣 ∈ 𝑆 ) → ( ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢 ) → ¬ 𝑤 ∈ { ( ∪ 𝐽 ∖ 𝑆 ) } ) )
71 57 70 jcad ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠 ) ∧ ( 𝑢 ⊆ ( 𝑠 ∪ { ( ∪ 𝐽 ∖ 𝑆 ) } ) ∧ 𝑢 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑢 ) ∧ 𝑣 ∈ 𝑆 ) → ( ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢 ) → ( 𝑤 ∈ 𝑢 ∧ ¬ 𝑤 ∈ { ( ∪ 𝐽 ∖ 𝑆 ) } ) ) )
72 eldif ⊢ ( 𝑤 ∈ ( 𝑢 ∖ { ( ∪ 𝐽 ∖ 𝑆 ) } ) ↔ ( 𝑤 ∈ 𝑢 ∧ ¬ 𝑤 ∈ { ( ∪ 𝐽 ∖ 𝑆 ) } ) )
73 71 72 imbitrrdi ⊢ ( ( ( ( ( 𝐽 ∈ 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 imbitrrdi ⊢ ( ( ( ( 𝐽 ∈ 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 biimtrid ⊢ ( ( 𝐽 ∈ 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 )