Metamath Proof Explorer


Theorem cmpsub

Description: Two equivalent ways of describing a compact subset of a topological space. Inspired by Sue E. Goodman'sBeginning Topology. (Contributed by Jeff Hankins, 22-Jun-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Hypothesis cmpsub.1 X = J
Assertion cmpsub J Top S X J 𝑡 S Comp c 𝒫 J S c d 𝒫 c Fin S d

Proof

Step Hyp Ref Expression
1 cmpsub.1 X = J
2 eqid J 𝑡 S = J 𝑡 S
3 2 iscmp J 𝑡 S Comp J 𝑡 S Top s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t
4 id S X S X
5 1 topopn J Top X J
6 ssexg S X X J S V
7 4 5 6 syl2anr J Top S X S V
8 resttop J Top S V J 𝑡 S Top
9 7 8 syldan J Top S X J 𝑡 S Top
10 ibar J 𝑡 S Top s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t J 𝑡 S Top s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t
11 10 bicomd J 𝑡 S Top J 𝑡 S Top s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t
12 9 11 syl J Top S X J 𝑡 S Top s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t
13 3 12 syl5bb J Top S X J 𝑡 S Comp s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t
14 vex t V
15 eqeq1 x = t x = y S t = y S
16 15 rexbidv x = t y c x = y S y c t = y S
17 14 16 elab t x | y c x = y S y c t = y S
18 velpw c 𝒫 J c J
19 ssel2 c J y c y J
20 ineq1 d = y d S = y S
21 20 rspceeqv y J t = y S d J t = d S
22 21 ex y J t = y S d J t = d S
23 19 22 syl c J y c t = y S d J t = d S
24 23 ex c J y c t = y S d J t = d S
25 18 24 sylbi c 𝒫 J y c t = y S d J t = d S
26 25 adantl J Top S X c 𝒫 J y c t = y S d J t = d S
27 26 rexlimdv J Top S X c 𝒫 J y c t = y S d J t = d S
28 simpll J Top S X c 𝒫 J J Top
29 1 sseq2i S X S J
30 uniexg J Top J V
31 ssexg S J J V S V
32 30 31 sylan2 S J J Top S V
33 32 ancoms J Top S J S V
34 29 33 sylan2b J Top S X S V
35 34 adantr J Top S X c 𝒫 J S V
36 elrest J Top S V t J 𝑡 S d J t = d S
37 28 35 36 syl2anc J Top S X c 𝒫 J t J 𝑡 S d J t = d S
38 27 37 sylibrd J Top S X c 𝒫 J y c t = y S t J 𝑡 S
39 17 38 syl5bi J Top S X c 𝒫 J t x | y c x = y S t J 𝑡 S
40 39 ssrdv J Top S X c 𝒫 J x | y c x = y S J 𝑡 S
41 vex c V
42 41 abrexex x | y c x = y S V
43 42 elpw x | y c x = y S 𝒫 J 𝑡 S x | y c x = y S J 𝑡 S
44 40 43 sylibr J Top S X c 𝒫 J x | y c x = y S 𝒫 J 𝑡 S
45 unieq s = x | y c x = y S s = x | y c x = y S
46 45 eqeq2d s = x | y c x = y S J 𝑡 S = s J 𝑡 S = x | y c x = y S
47 pweq s = x | y c x = y S 𝒫 s = 𝒫 x | y c x = y S
48 47 ineq1d s = x | y c x = y S 𝒫 s Fin = 𝒫 x | y c x = y S Fin
49 48 rexeqdv s = x | y c x = y S t 𝒫 s Fin J 𝑡 S = t t 𝒫 x | y c x = y S Fin J 𝑡 S = t
50 46 49 imbi12d s = x | y c x = y S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t J 𝑡 S = x | y c x = y S t 𝒫 x | y c x = y S Fin J 𝑡 S = t
51 50 rspcva x | y c x = y S 𝒫 J 𝑡 S s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t J 𝑡 S = x | y c x = y S t 𝒫 x | y c x = y S Fin J 𝑡 S = t
52 44 51 sylan J Top S X c 𝒫 J s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t J 𝑡 S = x | y c x = y S t 𝒫 x | y c x = y S Fin J 𝑡 S = t
53 52 ex J Top S X c 𝒫 J s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t J 𝑡 S = x | y c x = y S t 𝒫 x | y c x = y S Fin J 𝑡 S = t
54 1 restuni J Top S X S = J 𝑡 S
55 54 ad2antrr J Top S X c 𝒫 J S c S = J 𝑡 S
56 vex y V
57 56 inex1 y S V
58 57 dfiun2 y c y S = x | y c x = y S
59 incom y S = S y
60 59 a1i J Top S X c 𝒫 J S c y c y S = S y
61 60 iuneq2dv J Top S X c 𝒫 J S c y c y S = y c S y
62 58 61 eqtr3id J Top S X c 𝒫 J S c x | y c x = y S = y c S y
63 iunin2 y c S y = S y c y
64 uniiun c = y c y
65 64 eqcomi y c y = c
66 65 a1i J Top S X c 𝒫 J S c y c y = c
67 66 ineq2d J Top S X c 𝒫 J S c S y c y = S c
68 incom S c = c S
69 sseqin2 S c c S = S
70 69 biimpi S c c S = S
71 68 70 syl5eq S c S c = S
72 71 adantl J Top S X c 𝒫 J S c S c = S
73 67 72 eqtrd J Top S X c 𝒫 J S c S y c y = S
74 63 73 syl5eq J Top S X c 𝒫 J S c y c S y = S
75 62 74 eqtr2d J Top S X c 𝒫 J S c S = x | y c x = y S
76 55 75 eqeq12d J Top S X c 𝒫 J S c S = S J 𝑡 S = x | y c x = y S
77 55 eqeq1d J Top S X c 𝒫 J S c S = t J 𝑡 S = t
78 77 rexbidv J Top S X c 𝒫 J S c t 𝒫 x | y c x = y S Fin S = t t 𝒫 x | y c x = y S Fin J 𝑡 S = t
79 76 78 imbi12d J Top S X c 𝒫 J S c S = S t 𝒫 x | y c x = y S Fin S = t J 𝑡 S = x | y c x = y S t 𝒫 x | y c x = y S Fin J 𝑡 S = t
80 eqid S = S
81 80 a1bi t 𝒫 x | y c x = y S Fin S = t S = S t 𝒫 x | y c x = y S Fin S = t
82 elin t 𝒫 x | y c x = y S Fin t 𝒫 x | y c x = y S t Fin
83 velpw t 𝒫 x | y c x = y S t x | y c x = y S
84 dfss3 t x | y c x = y S s t s x | y c x = y S
85 vex s V
86 eqeq1 x = s x = y S s = y S
87 86 rexbidv x = s y c x = y S y c s = y S
88 85 87 elab s x | y c x = y S y c s = y S
89 88 ralbii s t s x | y c x = y S s t y c s = y S
90 83 84 89 3bitri t 𝒫 x | y c x = y S s t y c s = y S
91 90 anbi1i t 𝒫 x | y c x = y S t Fin s t y c s = y S t Fin
92 82 91 bitri t 𝒫 x | y c x = y S Fin s t y c s = y S t Fin
93 ineq1 y = f s y S = f s S
94 93 eqeq2d y = f s s = y S s = f s S
95 94 ac6sfi t Fin s t y c s = y S f f : t c s t s = f s S
96 95 ancoms s t y c s = y S t Fin f f : t c s t s = f s S
97 96 adantl 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
98 frn f : t c ran f c
99 98 ad2antrl 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
100 vex f V
101 100 rnex ran f V
102 101 elpw ran f 𝒫 c ran f c
103 99 102 sylibr 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
104 simprr J Top S X c 𝒫 J S c s t y c s = y S t Fin t Fin
105 104 ad2antrr 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
106 ffn f : t c f Fn t
107 dffn4 f Fn t f : t onto ran f
108 106 107 sylib f : t c f : t onto ran f
109 fodomfi t Fin f : t onto ran f ran f t
110 108 109 sylan2 t Fin f : t c ran f t
111 110 adantll s t y c s = y S t Fin f : t c ran f t
112 111 adantll J Top S X c 𝒫 J S c s t y c s = y S t Fin f : t c ran f t
113 112 ad2ant2r 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
114 domfi t Fin ran f t ran f Fin
115 105 113 114 syl2anc 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
116 103 115 elind 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
117 id s = u s = u
118 fveq2 s = u f s = f u
119 118 ineq1d s = u f s S = f u S
120 117 119 eqeq12d s = u s = f s S u = f u S
121 120 rspccv s t s = f s S u t u = f u S
122 pm2.27 u t u t u = f u S u = f u S
123 inss1 f u S f u
124 sseq1 u = f u S u f u f u S f u
125 123 124 mpbiri u = f u S u f u
126 ssel u f u w u w f u
127 126 a1dd u f u w u f : t c w f u
128 125 127 syl u = f u S w u f : t c w f u
129 128 a1i u t u = f u S w u f : t c w f u
130 129 3imp u t u = f u S w u f : t c w f u
131 fnfvelrn f Fn t u t f u ran f
132 131 expcom u t f Fn t f u ran f
133 132 3ad2ant1 u t u = f u S w u f Fn t f u ran f
134 106 133 syl5 u t u = f u S w u f : t c f u ran f
135 130 134 jcad u t u = f u S w u f : t c w f u f u ran f
136 135 3exp u t u = f u S w u f : t c w f u f u ran f
137 122 136 syld u t u t u = f u S w u f : t c w f u f u ran f
138 137 com3r w u u t u t u = f u S f : t c w f u f u ran f
139 138 imp w u u t u t u = f u S f : t c w f u f u ran f
140 139 com3l u t u = f u S f : t c w u u t w f u f u ran f
141 140 impcom f : t c u t u = f u S w u u t w f u f u ran f
142 121 141 sylan2 f : t c s t s = f s S w u u t w f u f u ran f
143 fvex f u V
144 eleq2 v = f u w v w f u
145 eleq1 v = f u v ran f f u ran f
146 144 145 anbi12d v = f u w v v ran f w f u f u ran f
147 143 146 spcev w f u f u ran f v w v v ran f
148 142 147 syl6 f : t c s t s = f s S w u u t v w v v ran f
149 148 exlimdv f : t c s t s = f s S u w u u t v w v v ran f
150 eluni w t u w u u t
151 eluni w ran f v w v v ran f
152 149 150 151 3imtr4g f : t c s t s = f s S w t w ran f
153 152 ssrdv f : t c s t s = f s S t ran f
154 153 adantl 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
155 sseq1 S = t S ran f t ran f
156 155 ad2antlr 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
157 154 156 mpbird 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
158 116 157 jca 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
159 158 ex 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
160 159 eximdv 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
161 160 ex 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
162 161 com23 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
163 unieq d = ran f d = ran f
164 163 sseq2d d = ran f S d S ran f
165 164 rspcev ran f 𝒫 c Fin S ran f d 𝒫 c Fin S d
166 165 exlimiv f ran f 𝒫 c Fin S ran f d 𝒫 c Fin S d
167 162 166 syl8 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
168 97 167 mpd J Top S X c 𝒫 J S c s t y c s = y S t Fin S = t d 𝒫 c Fin S d
169 92 168 sylan2b J Top S X c 𝒫 J S c t 𝒫 x | y c x = y S Fin S = t d 𝒫 c Fin S d
170 169 rexlimdva J Top S X c 𝒫 J S c t 𝒫 x | y c x = y S Fin S = t d 𝒫 c Fin S d
171 81 170 syl5bir 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
172 79 171 sylbird J Top S X c 𝒫 J S c J 𝑡 S = x | y c x = y S t 𝒫 x | y c x = y S Fin J 𝑡 S = t d 𝒫 c Fin S d
173 172 ex J Top S X c 𝒫 J S c J 𝑡 S = x | y c x = y S t 𝒫 x | y c x = y S Fin J 𝑡 S = t d 𝒫 c Fin S d
174 173 com23 J Top S X c 𝒫 J J 𝑡 S = x | y c x = y S t 𝒫 x | y c x = y S Fin J 𝑡 S = t S c d 𝒫 c Fin S d
175 53 174 syld J Top S X c 𝒫 J s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t S c d 𝒫 c Fin S d
176 175 ralrimdva J Top S X s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t c 𝒫 J S c d 𝒫 c Fin S d
177 1 cmpsublem J Top S X c 𝒫 J S c d 𝒫 c Fin S d s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t
178 176 177 impbid J Top S X s 𝒫 J 𝑡 S J 𝑡 S = s t 𝒫 s Fin J 𝑡 S = t c 𝒫 J S c d 𝒫 c Fin S d
179 13 178 bitrd J Top S X J 𝑡 S Comp c 𝒫 J S c d 𝒫 c Fin S d