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 JTopSXJ𝑡SCompc𝒫JScd𝒫cFinSd

Proof

Step Hyp Ref Expression
1 cmpsub.1 X=J
2 eqid J𝑡S=J𝑡S
3 2 iscmp J𝑡SCompJ𝑡STops𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=t
4 id SXSX
5 1 topopn JTopXJ
6 ssexg SXXJSV
7 4 5 6 syl2anr JTopSXSV
8 resttop JTopSVJ𝑡STop
9 7 8 syldan JTopSXJ𝑡STop
10 ibar J𝑡STops𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=tJ𝑡STops𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=t
11 10 bicomd J𝑡STopJ𝑡STops𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=ts𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=t
12 9 11 syl JTopSXJ𝑡STops𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=ts𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=t
13 3 12 bitrid JTopSXJ𝑡SComps𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=t
14 vex tV
15 eqeq1 x=tx=ySt=yS
16 15 rexbidv x=tycx=ySyct=yS
17 14 16 elab tx|ycx=ySyct=yS
18 velpw c𝒫JcJ
19 ssel2 cJycyJ
20 ineq1 d=ydS=yS
21 20 rspceeqv yJt=ySdJt=dS
22 21 ex yJt=ySdJt=dS
23 19 22 syl cJyct=ySdJt=dS
24 23 ex cJyct=ySdJt=dS
25 18 24 sylbi c𝒫Jyct=ySdJt=dS
26 25 adantl JTopSXc𝒫Jyct=ySdJt=dS
27 26 rexlimdv JTopSXc𝒫Jyct=ySdJt=dS
28 simpll JTopSXc𝒫JJTop
29 1 sseq2i SXSJ
30 uniexg JTopJV
31 ssexg SJJVSV
32 30 31 sylan2 SJJTopSV
33 32 ancoms JTopSJSV
34 29 33 sylan2b JTopSXSV
35 34 adantr JTopSXc𝒫JSV
36 elrest JTopSVtJ𝑡SdJt=dS
37 28 35 36 syl2anc JTopSXc𝒫JtJ𝑡SdJt=dS
38 27 37 sylibrd JTopSXc𝒫Jyct=yStJ𝑡S
39 17 38 biimtrid JTopSXc𝒫Jtx|ycx=yStJ𝑡S
40 39 ssrdv JTopSXc𝒫Jx|ycx=ySJ𝑡S
41 vex cV
42 41 abrexex x|ycx=ySV
43 42 elpw x|ycx=yS𝒫J𝑡Sx|ycx=ySJ𝑡S
44 40 43 sylibr JTopSXc𝒫Jx|ycx=yS𝒫J𝑡S
45 unieq s=x|ycx=ySs=x|ycx=yS
46 45 eqeq2d s=x|ycx=ySJ𝑡S=sJ𝑡S=x|ycx=yS
47 pweq s=x|ycx=yS𝒫s=𝒫x|ycx=yS
48 47 ineq1d s=x|ycx=yS𝒫sFin=𝒫x|ycx=ySFin
49 48 rexeqdv s=x|ycx=ySt𝒫sFinJ𝑡S=tt𝒫x|ycx=ySFinJ𝑡S=t
50 46 49 imbi12d s=x|ycx=ySJ𝑡S=st𝒫sFinJ𝑡S=tJ𝑡S=x|ycx=ySt𝒫x|ycx=ySFinJ𝑡S=t
51 50 rspcva x|ycx=yS𝒫J𝑡Ss𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=tJ𝑡S=x|ycx=ySt𝒫x|ycx=ySFinJ𝑡S=t
52 44 51 sylan JTopSXc𝒫Js𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=tJ𝑡S=x|ycx=ySt𝒫x|ycx=ySFinJ𝑡S=t
53 52 ex JTopSXc𝒫Js𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=tJ𝑡S=x|ycx=ySt𝒫x|ycx=ySFinJ𝑡S=t
54 1 restuni JTopSXS=J𝑡S
55 54 ad2antrr JTopSXc𝒫JScS=J𝑡S
56 vex yV
57 56 inex1 ySV
58 57 dfiun2 ycyS=x|ycx=yS
59 incom yS=Sy
60 59 a1i JTopSXc𝒫JScycyS=Sy
61 60 iuneq2dv JTopSXc𝒫JScycyS=ycSy
62 58 61 eqtr3id JTopSXc𝒫JScx|ycx=yS=ycSy
63 iunin2 ycSy=Sycy
64 uniiun c=ycy
65 64 eqcomi ycy=c
66 65 a1i JTopSXc𝒫JScycy=c
67 66 ineq2d JTopSXc𝒫JScSycy=Sc
68 incom Sc=cS
69 sseqin2 SccS=S
70 69 biimpi SccS=S
71 68 70 eqtrid ScSc=S
72 71 adantl JTopSXc𝒫JScSc=S
73 67 72 eqtrd JTopSXc𝒫JScSycy=S
74 63 73 eqtrid JTopSXc𝒫JScycSy=S
75 62 74 eqtr2d JTopSXc𝒫JScS=x|ycx=yS
76 55 75 eqeq12d JTopSXc𝒫JScS=SJ𝑡S=x|ycx=yS
77 55 eqeq1d JTopSXc𝒫JScS=tJ𝑡S=t
78 77 rexbidv JTopSXc𝒫JSct𝒫x|ycx=ySFinS=tt𝒫x|ycx=ySFinJ𝑡S=t
79 76 78 imbi12d JTopSXc𝒫JScS=St𝒫x|ycx=ySFinS=tJ𝑡S=x|ycx=ySt𝒫x|ycx=ySFinJ𝑡S=t
80 eqid S=S
81 80 a1bi t𝒫x|ycx=ySFinS=tS=St𝒫x|ycx=ySFinS=t
82 elin t𝒫x|ycx=ySFint𝒫x|ycx=yStFin
83 velpw t𝒫x|ycx=yStx|ycx=yS
84 dfss3 tx|ycx=ySstsx|ycx=yS
85 vex sV
86 eqeq1 x=sx=ySs=yS
87 86 rexbidv x=sycx=ySycs=yS
88 85 87 elab sx|ycx=ySycs=yS
89 88 ralbii stsx|ycx=ySstycs=yS
90 83 84 89 3bitri t𝒫x|ycx=ySstycs=yS
91 90 anbi1i t𝒫x|ycx=yStFinstycs=yStFin
92 82 91 bitri t𝒫x|ycx=ySFinstycs=yStFin
93 ineq1 y=fsyS=fsS
94 93 eqeq2d y=fss=ySs=fsS
95 94 ac6sfi tFinstycs=ySff:tcsts=fsS
96 95 ancoms stycs=yStFinff:tcsts=fsS
97 96 adantl JTopSXc𝒫JScstycs=yStFinff:tcsts=fsS
98 frn f:tcranfc
99 98 ad2antrl JTopSXc𝒫JScstycs=yStFinS=tf:tcsts=fsSranfc
100 vex fV
101 100 rnex ranfV
102 101 elpw ranf𝒫cranfc
103 99 102 sylibr JTopSXc𝒫JScstycs=yStFinS=tf:tcsts=fsSranf𝒫c
104 simprr JTopSXc𝒫JScstycs=yStFintFin
105 104 ad2antrr JTopSXc𝒫JScstycs=yStFinS=tf:tcsts=fsStFin
106 ffn f:tcfFnt
107 dffn4 fFntf:tontoranf
108 106 107 sylib f:tcf:tontoranf
109 fodomfi tFinf:tontoranfranft
110 108 109 sylan2 tFinf:tcranft
111 110 adantll stycs=yStFinf:tcranft
112 111 adantll JTopSXc𝒫JScstycs=yStFinf:tcranft
113 112 ad2ant2r JTopSXc𝒫JScstycs=yStFinS=tf:tcsts=fsSranft
114 domfi tFinranftranfFin
115 105 113 114 syl2anc JTopSXc𝒫JScstycs=yStFinS=tf:tcsts=fsSranfFin
116 103 115 elind JTopSXc𝒫JScstycs=yStFinS=tf:tcsts=fsSranf𝒫cFin
117 id s=us=u
118 fveq2 s=ufs=fu
119 118 ineq1d s=ufsS=fuS
120 117 119 eqeq12d s=us=fsSu=fuS
121 120 rspccv sts=fsSutu=fuS
122 pm2.27 ututu=fuSu=fuS
123 inss1 fuSfu
124 sseq1 u=fuSufufuSfu
125 123 124 mpbiri u=fuSufu
126 ssel ufuwuwfu
127 126 a1dd ufuwuf:tcwfu
128 125 127 syl u=fuSwuf:tcwfu
129 128 a1i utu=fuSwuf:tcwfu
130 129 3imp utu=fuSwuf:tcwfu
131 fnfvelrn fFntutfuranf
132 131 expcom utfFntfuranf
133 132 3ad2ant1 utu=fuSwufFntfuranf
134 106 133 syl5 utu=fuSwuf:tcfuranf
135 130 134 jcad utu=fuSwuf:tcwfufuranf
136 135 3exp utu=fuSwuf:tcwfufuranf
137 122 136 syld ututu=fuSwuf:tcwfufuranf
138 137 com3r wuututu=fuSf:tcwfufuranf
139 138 imp wuututu=fuSf:tcwfufuranf
140 139 com3l utu=fuSf:tcwuutwfufuranf
141 140 impcom f:tcutu=fuSwuutwfufuranf
142 121 141 sylan2 f:tcsts=fsSwuutwfufuranf
143 fvex fuV
144 eleq2 v=fuwvwfu
145 eleq1 v=fuvranffuranf
146 144 145 anbi12d v=fuwvvranfwfufuranf
147 143 146 spcev wfufuranfvwvvranf
148 142 147 syl6 f:tcsts=fsSwuutvwvvranf
149 148 exlimdv f:tcsts=fsSuwuutvwvvranf
150 eluni wtuwuut
151 eluni wranfvwvvranf
152 149 150 151 3imtr4g f:tcsts=fsSwtwranf
153 152 ssrdv f:tcsts=fsStranf
154 153 adantl JTopSXc𝒫JScstycs=yStFinS=tf:tcsts=fsStranf
155 sseq1 S=tSranftranf
156 155 ad2antlr JTopSXc𝒫JScstycs=yStFinS=tf:tcsts=fsSSranftranf
157 154 156 mpbird JTopSXc𝒫JScstycs=yStFinS=tf:tcsts=fsSSranf
158 116 157 jca JTopSXc𝒫JScstycs=yStFinS=tf:tcsts=fsSranf𝒫cFinSranf
159 158 ex JTopSXc𝒫JScstycs=yStFinS=tf:tcsts=fsSranf𝒫cFinSranf
160 159 eximdv JTopSXc𝒫JScstycs=yStFinS=tff:tcsts=fsSfranf𝒫cFinSranf
161 160 ex JTopSXc𝒫JScstycs=yStFinS=tff:tcsts=fsSfranf𝒫cFinSranf
162 161 com23 JTopSXc𝒫JScstycs=yStFinff:tcsts=fsSS=tfranf𝒫cFinSranf
163 unieq d=ranfd=ranf
164 163 sseq2d d=ranfSdSranf
165 164 rspcev ranf𝒫cFinSranfd𝒫cFinSd
166 165 exlimiv franf𝒫cFinSranfd𝒫cFinSd
167 162 166 syl8 JTopSXc𝒫JScstycs=yStFinff:tcsts=fsSS=td𝒫cFinSd
168 97 167 mpd JTopSXc𝒫JScstycs=yStFinS=td𝒫cFinSd
169 92 168 sylan2b JTopSXc𝒫JSct𝒫x|ycx=ySFinS=td𝒫cFinSd
170 169 rexlimdva JTopSXc𝒫JSct𝒫x|ycx=ySFinS=td𝒫cFinSd
171 81 170 biimtrrid JTopSXc𝒫JScS=St𝒫x|ycx=ySFinS=td𝒫cFinSd
172 79 171 sylbird JTopSXc𝒫JScJ𝑡S=x|ycx=ySt𝒫x|ycx=ySFinJ𝑡S=td𝒫cFinSd
173 172 ex JTopSXc𝒫JScJ𝑡S=x|ycx=ySt𝒫x|ycx=ySFinJ𝑡S=td𝒫cFinSd
174 173 com23 JTopSXc𝒫JJ𝑡S=x|ycx=ySt𝒫x|ycx=ySFinJ𝑡S=tScd𝒫cFinSd
175 53 174 syld JTopSXc𝒫Js𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=tScd𝒫cFinSd
176 175 ralrimdva JTopSXs𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=tc𝒫JScd𝒫cFinSd
177 1 cmpsublem JTopSXc𝒫JScd𝒫cFinSds𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=t
178 176 177 impbid JTopSXs𝒫J𝑡SJ𝑡S=st𝒫sFinJ𝑡S=tc𝒫JScd𝒫cFinSd
179 13 178 bitrd JTopSXJ𝑡SCompc𝒫JScd𝒫cFinSd