Metamath Proof Explorer


Theorem comppfsc

Description: A space where every open cover has a point-finite subcover is compact. This is significant in part because it shows half of the proposition that if only half the generalization in the definition of metacompactness (and consequently paracompactness) is performed, one does not obtain any more spaces. (Contributed by Jeff Hankins, 21-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypothesis comppfsc.1 X=J
Assertion comppfsc JTopJCompc𝒫JX=cdPtFindcX=d

Proof

Step Hyp Ref Expression
1 comppfsc.1 X=J
2 elpwi c𝒫JcJ
3 1 cmpcov JCompcJX=cd𝒫cFinX=d
4 elfpw d𝒫cFindcdFin
5 finptfin dFindPtFin
6 5 anim1i dFindcX=ddPtFindcX=d
7 6 anassrs dFindcX=ddPtFindcX=d
8 7 ancom1s dcdFinX=ddPtFindcX=d
9 4 8 sylanb d𝒫cFinX=ddPtFindcX=d
10 9 reximi2 d𝒫cFinX=ddPtFindcX=d
11 3 10 syl JCompcJX=cdPtFindcX=d
12 11 3exp JCompcJX=cdPtFindcX=d
13 2 12 syl5 JCompc𝒫JX=cdPtFindcX=d
14 13 ralrimiv JCompc𝒫JX=cdPtFindcX=d
15 elpwi a𝒫JaJ
16 0elpw 𝒫a
17 0fin Fin
18 16 17 elini 𝒫aFin
19 unieq b=b=
20 uni0 =
21 19 20 eqtrdi b=b=
22 21 rspceeqv 𝒫aFinX=b𝒫aFinX=b
23 18 22 mpan X=b𝒫aFinX=b
24 23 a1i13 JTopX=aaJX=c𝒫JX=cdPtFindcX=db𝒫aFinX=b
25 n0 XxxX
26 simp2 JTopX=aaJX=a
27 26 eleq2d JTopX=aaJxXxa
28 27 biimpd JTopX=aaJxXxa
29 eluni2 xasaxs
30 28 29 imbitrdi JTopX=aaJxXsaxs
31 simpl3 JTopX=aaJsaxsaJ
32 simprl JTopX=aaJsaxssa
33 31 32 sseldd JTopX=aaJsaxssJ
34 elssuni sJsJ
35 34 1 sseqtrrdi sJsX
36 33 35 syl JTopX=aaJsaxssX
37 36 ralrimivw JTopX=aaJsaxspasX
38 iunss pasXpasX
39 37 38 sylibr JTopX=aaJsaxspasX
40 ssequn1 pasXpasX=X
41 39 40 sylib JTopX=aaJsaxspasX=X
42 simpl2 JTopX=aaJsaxsX=a
43 uniiun a=pap
44 42 43 eqtrdi JTopX=aaJsaxsX=pap
45 44 uneq2d JTopX=aaJsaxspasX=paspap
46 41 45 eqtr3d JTopX=aaJsaxsX=paspap
47 iunun pasp=paspap
48 vex sV
49 vex pV
50 48 49 unex spV
51 50 dfiun3 pasp=ranpasp
52 47 51 eqtr3i paspap=ranpasp
53 46 52 eqtrdi JTopX=aaJsaxsX=ranpasp
54 simpll1 JTopX=aaJsaxspaJTop
55 33 adantr JTopX=aaJsaxspasJ
56 31 sselda JTopX=aaJsaxspapJ
57 unopn JTopsJpJspJ
58 54 55 56 57 syl3anc JTopX=aaJsaxspaspJ
59 58 fmpttd JTopX=aaJsaxspasp:aJ
60 59 frnd JTopX=aaJsaxsranpaspJ
61 elpw2g JTopranpasp𝒫JranpaspJ
62 61 3ad2ant1 JTopX=aaJranpasp𝒫JranpaspJ
63 62 adantr JTopX=aaJsaxsranpasp𝒫JranpaspJ
64 60 63 mpbird JTopX=aaJsaxsranpasp𝒫J
65 unieq c=ranpaspc=ranpasp
66 65 eqeq2d c=ranpaspX=cX=ranpasp
67 sseq2 c=ranpaspdcdranpasp
68 67 anbi1d c=ranpaspdcX=ddranpaspX=d
69 68 rexbidv c=ranpaspdPtFindcX=ddPtFindranpaspX=d
70 66 69 imbi12d c=ranpaspX=cdPtFindcX=dX=ranpaspdPtFindranpaspX=d
71 70 rspcv ranpasp𝒫Jc𝒫JX=cdPtFindcX=dX=ranpaspdPtFindranpaspX=d
72 64 71 syl JTopX=aaJsaxsc𝒫JX=cdPtFindcX=dX=ranpaspdPtFindranpaspX=d
73 53 72 mpid JTopX=aaJsaxsc𝒫JX=cdPtFindcX=ddPtFindranpaspX=d
74 simprr JTopX=aaJsaxsxs
75 ssel2 aJsasJ
76 75 3ad2antl3 JTopX=aaJsasJ
77 76 adantrr JTopX=aaJsaxssJ
78 elunii xssJxJ
79 74 77 78 syl2anc JTopX=aaJsaxsxJ
80 79 1 eleqtrrdi JTopX=aaJsaxsxX
81 80 adantr JTopX=aaJsaxsdranpaspX=dxX
82 simprr JTopX=aaJsaxsdranpaspX=dX=d
83 81 82 eleqtrd JTopX=aaJsaxsdranpaspX=dxd
84 eqid d=d
85 84 ptfinfin dPtFinxdzd|xzFin
86 85 expcom xddPtFinzd|xzFin
87 83 86 syl JTopX=aaJsaxsdranpaspX=ddPtFinzd|xzFin
88 simprl JTopX=aaJsaxsdranpaspX=ddranpasp
89 elun1 xsxsp
90 89 ad2antll JTopX=aaJsaxsxsp
91 90 ralrimivw JTopX=aaJsaxspaxsp
92 50 rgenw paspV
93 eqid pasp=pasp
94 eleq2 z=spxzxsp
95 93 94 ralrnmptw paspVzranpaspxzpaxsp
96 92 95 ax-mp zranpaspxzpaxsp
97 91 96 sylibr JTopX=aaJsaxszranpaspxz
98 97 adantr JTopX=aaJsaxsdranpaspX=dzranpaspxz
99 ssralv dranpaspzranpaspxzzdxz
100 88 98 99 sylc JTopX=aaJsaxsdranpaspX=dzdxz
101 rabid2 d=zd|xzzdxz
102 100 101 sylibr JTopX=aaJsaxsdranpaspX=dd=zd|xz
103 102 eleq1d JTopX=aaJsaxsdranpaspX=ddFinzd|xzFin
104 103 biimprd JTopX=aaJsaxsdranpaspX=dzd|xzFindFin
105 93 rnmpt ranpasp=q|paq=sp
106 88 105 sseqtrdi JTopX=aaJsaxsdranpaspX=ddq|paq=sp
107 ssabral dq|paq=spqdpaq=sp
108 106 107 sylib JTopX=aaJsaxsdranpaspX=dqdpaq=sp
109 uneq2 p=fqsp=sfq
110 109 eqeq2d p=fqq=spq=sfq
111 110 ac6sfi dFinqdpaq=spff:daqdq=sfq
112 111 expcom qdpaq=spdFinff:daqdq=sfq
113 108 112 syl JTopX=aaJsaxsdranpaspX=ddFinff:daqdq=sfq
114 frn f:daranfa
115 114 adantr f:daqdq=sfqranfa
116 115 ad2antll JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqranfa
117 32 ad2antrr JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqsa
118 117 snssd JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqsa
119 116 118 unssd JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqranfsa
120 simprl JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqdFin
121 simprrl JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqf:da
122 121 ffnd JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqfFnd
123 dffn4 fFndf:dontoranf
124 122 123 sylib JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqf:dontoranf
125 fofi dFinf:dontoranfranfFin
126 120 124 125 syl2anc JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqranfFin
127 snfi sFin
128 unfi ranfFinsFinranfsFin
129 126 127 128 sylancl JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqranfsFin
130 elfpw ranfs𝒫aFinranfsaranfsFin
131 119 129 130 sylanbrc JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqranfs𝒫aFin
132 simplrr JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqX=d
133 uniiun d=qdq
134 simprrr JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqqdq=sfq
135 iuneq2 qdq=sfqqdq=qdsfq
136 134 135 syl JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqqdq=qdsfq
137 133 136 eqtrid JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqd=qdsfq
138 132 137 eqtrd JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqX=qdsfq
139 ssun2 sranfs
140 vsnid ss
141 139 140 sselii sranfs
142 elssuni sranfssranfs
143 141 142 ax-mp sranfs
144 fvssunirn fqranf
145 ssun1 ranfranfs
146 145 unissi ranfranfs
147 144 146 sstri fqranfs
148 143 147 unssi sfqranfs
149 148 rgenw qdsfqranfs
150 iunss qdsfqranfsqdsfqranfs
151 149 150 mpbir qdsfqranfs
152 138 151 eqsstrdi JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqXranfs
153 31 ad2antrr JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqaJ
154 116 153 sstrd JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqranfJ
155 33 ad2antrr JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqsJ
156 155 snssd JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqsJ
157 154 156 unssd JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqranfsJ
158 uniss ranfsJranfsJ
159 158 1 sseqtrrdi ranfsJranfsX
160 157 159 syl JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqranfsX
161 152 160 eqssd JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqX=ranfs
162 unieq b=ranfsb=ranfs
163 162 rspceeqv ranfs𝒫aFinX=ranfsb𝒫aFinX=b
164 131 161 163 syl2anc JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqb𝒫aFinX=b
165 164 expr JTopX=aaJsaxsdranpaspX=ddFinf:daqdq=sfqb𝒫aFinX=b
166 165 exlimdv JTopX=aaJsaxsdranpaspX=ddFinff:daqdq=sfqb𝒫aFinX=b
167 166 ex JTopX=aaJsaxsdranpaspX=ddFinff:daqdq=sfqb𝒫aFinX=b
168 113 167 mpdd JTopX=aaJsaxsdranpaspX=ddFinb𝒫aFinX=b
169 87 104 168 3syld JTopX=aaJsaxsdranpaspX=ddPtFinb𝒫aFinX=b
170 169 ex JTopX=aaJsaxsdranpaspX=ddPtFinb𝒫aFinX=b
171 170 com23 JTopX=aaJsaxsdPtFindranpaspX=db𝒫aFinX=b
172 171 rexlimdv JTopX=aaJsaxsdPtFindranpaspX=db𝒫aFinX=b
173 73 172 syld JTopX=aaJsaxsc𝒫JX=cdPtFindcX=db𝒫aFinX=b
174 173 rexlimdvaa JTopX=aaJsaxsc𝒫JX=cdPtFindcX=db𝒫aFinX=b
175 30 174 syld JTopX=aaJxXc𝒫JX=cdPtFindcX=db𝒫aFinX=b
176 175 exlimdv JTopX=aaJxxXc𝒫JX=cdPtFindcX=db𝒫aFinX=b
177 25 176 biimtrid JTopX=aaJXc𝒫JX=cdPtFindcX=db𝒫aFinX=b
178 24 177 pm2.61dne JTopX=aaJc𝒫JX=cdPtFindcX=db𝒫aFinX=b
179 15 178 syl3an3 JTopX=aa𝒫Jc𝒫JX=cdPtFindcX=db𝒫aFinX=b
180 179 3exp JTopX=aa𝒫Jc𝒫JX=cdPtFindcX=db𝒫aFinX=b
181 180 com24 JTopc𝒫JX=cdPtFindcX=da𝒫JX=ab𝒫aFinX=b
182 181 ralrimdv JTopc𝒫JX=cdPtFindcX=da𝒫JX=ab𝒫aFinX=b
183 1 iscmp JCompJTopa𝒫JX=ab𝒫aFinX=b
184 183 baibr JTopa𝒫JX=ab𝒫aFinX=bJComp
185 182 184 sylibd JTopc𝒫JX=cdPtFindcX=dJComp
186 14 185 impbid2 JTopJCompc𝒫JX=cdPtFindcX=d