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 J Comp S Clsd J J 𝑡 S Comp

Proof

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