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 J Top J Comp c 𝒫 J X = c d PtFin d c X = d

Proof

Step Hyp Ref Expression
1 comppfsc.1 X = J
2 elpwi c 𝒫 J c J
3 1 cmpcov J Comp c J X = c d 𝒫 c Fin X = d
4 elfpw d 𝒫 c Fin d c d Fin
5 finptfin d Fin d PtFin
6 5 anim1i d Fin d c X = d d PtFin d c X = d
7 6 anassrs d Fin d c X = d d PtFin d c X = d
8 7 ancom1s d c d Fin X = d d PtFin d c X = d
9 4 8 sylanb d 𝒫 c Fin X = d d PtFin d c X = d
10 9 reximi2 d 𝒫 c Fin X = d d PtFin d c X = d
11 3 10 syl J Comp c J X = c d PtFin d c X = d
12 11 3exp J Comp c J X = c d PtFin d c X = d
13 2 12 syl5 J Comp c 𝒫 J X = c d PtFin d c X = d
14 13 ralrimiv J Comp c 𝒫 J X = c d PtFin d c X = d
15 elpwi a 𝒫 J a J
16 0elpw 𝒫 a
17 0fin Fin
18 16 17 elini 𝒫 a Fin
19 unieq b = b =
20 uni0 =
21 19 20 eqtrdi b = b =
22 21 rspceeqv 𝒫 a Fin X = b 𝒫 a Fin X = b
23 18 22 mpan X = b 𝒫 a Fin X = b
24 23 a1i13 J Top X = a a J X = c 𝒫 J X = c d PtFin d c X = d b 𝒫 a Fin X = b
25 n0 X x x X
26 simp2 J Top X = a a J X = a
27 26 eleq2d J Top X = a a J x X x a
28 27 biimpd J Top X = a a J x X x a
29 eluni2 x a s a x s
30 28 29 syl6ib J Top X = a a J x X s a x s
31 simpl3 J Top X = a a J s a x s a J
32 simprl J Top X = a a J s a x s s a
33 31 32 sseldd J Top X = a a J s a x s s J
34 elssuni s J s J
35 34 1 sseqtrrdi s J s X
36 33 35 syl J Top X = a a J s a x s s X
37 36 ralrimivw J Top X = a a J s a x s p a s X
38 iunss p a s X p a s X
39 37 38 sylibr J Top X = a a J s a x s p a s X
40 ssequn1 p a s X p a s X = X
41 39 40 sylib J Top X = a a J s a x s p a s X = X
42 simpl2 J Top X = a a J s a x s X = a
43 uniiun a = p a p
44 42 43 eqtrdi J Top X = a a J s a x s X = p a p
45 44 uneq2d J Top X = a a J s a x s p a s X = p a s p a p
46 41 45 eqtr3d J Top X = a a J s a x s X = p a s p a p
47 iunun p a s p = p a s p a p
48 vex s V
49 vex p V
50 48 49 unex s p V
51 50 dfiun3 p a s p = ran p a s p
52 47 51 eqtr3i p a s p a p = ran p a s p
53 46 52 eqtrdi J Top X = a a J s a x s X = ran p a s p
54 simpll1 J Top X = a a J s a x s p a J Top
55 33 adantr J Top X = a a J s a x s p a s J
56 31 sselda J Top X = a a J s a x s p a p J
57 unopn J Top s J p J s p J
58 54 55 56 57 syl3anc J Top X = a a J s a x s p a s p J
59 58 fmpttd J Top X = a a J s a x s p a s p : a J
60 59 frnd J Top X = a a J s a x s ran p a s p J
61 elpw2g J Top ran p a s p 𝒫 J ran p a s p J
62 61 3ad2ant1 J Top X = a a J ran p a s p 𝒫 J ran p a s p J
63 62 adantr J Top X = a a J s a x s ran p a s p 𝒫 J ran p a s p J
64 60 63 mpbird J Top X = a a J s a x s ran p a s p 𝒫 J
65 unieq c = ran p a s p c = ran p a s p
66 65 eqeq2d c = ran p a s p X = c X = ran p a s p
67 sseq2 c = ran p a s p d c d ran p a s p
68 67 anbi1d c = ran p a s p d c X = d d ran p a s p X = d
69 68 rexbidv c = ran p a s p d PtFin d c X = d d PtFin d ran p a s p X = d
70 66 69 imbi12d c = ran p a s p X = c d PtFin d c X = d X = ran p a s p d PtFin d ran p a s p X = d
71 70 rspcv ran p a s p 𝒫 J c 𝒫 J X = c d PtFin d c X = d X = ran p a s p d PtFin d ran p a s p X = d
72 64 71 syl J Top X = a a J s a x s c 𝒫 J X = c d PtFin d c X = d X = ran p a s p d PtFin d ran p a s p X = d
73 53 72 mpid J Top X = a a J s a x s c 𝒫 J X = c d PtFin d c X = d d PtFin d ran p a s p X = d
74 simprr J Top X = a a J s a x s x s
75 ssel2 a J s a s J
76 75 3ad2antl3 J Top X = a a J s a s J
77 76 adantrr J Top X = a a J s a x s s J
78 elunii x s s J x J
79 74 77 78 syl2anc J Top X = a a J s a x s x J
80 79 1 eleqtrrdi J Top X = a a J s a x s x X
81 80 adantr J Top X = a a J s a x s d ran p a s p X = d x X
82 simprr J Top X = a a J s a x s d ran p a s p X = d X = d
83 81 82 eleqtrd J Top X = a a J s a x s d ran p a s p X = d x d
84 eqid d = d
85 84 ptfinfin d PtFin x d z d | x z Fin
86 85 expcom x d d PtFin z d | x z Fin
87 83 86 syl J Top X = a a J s a x s d ran p a s p X = d d PtFin z d | x z Fin
88 simprl J Top X = a a J s a x s d ran p a s p X = d d ran p a s p
89 elun1 x s x s p
90 89 ad2antll J Top X = a a J s a x s x s p
91 90 ralrimivw J Top X = a a J s a x s p a x s p
92 50 rgenw p a s p V
93 eqid p a s p = p a s p
94 eleq2 z = s p x z x s p
95 93 94 ralrnmptw p a s p V z ran p a s p x z p a x s p
96 92 95 ax-mp z ran p a s p x z p a x s p
97 91 96 sylibr J Top X = a a J s a x s z ran p a s p x z
98 97 adantr J Top X = a a J s a x s d ran p a s p X = d z ran p a s p x z
99 ssralv d ran p a s p z ran p a s p x z z d x z
100 88 98 99 sylc J Top X = a a J s a x s d ran p a s p X = d z d x z
101 rabid2 d = z d | x z z d x z
102 100 101 sylibr J Top X = a a J s a x s d ran p a s p X = d d = z d | x z
103 102 eleq1d J Top X = a a J s a x s d ran p a s p X = d d Fin z d | x z Fin
104 103 biimprd J Top X = a a J s a x s d ran p a s p X = d z d | x z Fin d Fin
105 93 rnmpt ran p a s p = q | p a q = s p
106 88 105 sseqtrdi J Top X = a a J s a x s d ran p a s p X = d d q | p a q = s p
107 ssabral d q | p a q = s p q d p a q = s p
108 106 107 sylib J Top X = a a J s a x s d ran p a s p X = d q d p a q = s p
109 uneq2 p = f q s p = s f q
110 109 eqeq2d p = f q q = s p q = s f q
111 110 ac6sfi d Fin q d p a q = s p f f : d a q d q = s f q
112 111 expcom q d p a q = s p d Fin f f : d a q d q = s f q
113 108 112 syl J Top X = a a J s a x s d ran p a s p X = d d Fin f f : d a q d q = s f q
114 frn f : d a ran f a
115 114 adantr f : d a q d q = s f q ran f a
116 115 ad2antll J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q ran f a
117 32 ad2antrr J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q s a
118 117 snssd J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q s a
119 116 118 unssd J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q ran f s a
120 simprl J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q d Fin
121 simprrl J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q f : d a
122 121 ffnd J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q f Fn d
123 dffn4 f Fn d f : d onto ran f
124 122 123 sylib J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q f : d onto ran f
125 fofi d Fin f : d onto ran f ran f Fin
126 120 124 125 syl2anc J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q ran f Fin
127 snfi s Fin
128 unfi ran f Fin s Fin ran f s Fin
129 126 127 128 sylancl J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q ran f s Fin
130 elfpw ran f s 𝒫 a Fin ran f s a ran f s Fin
131 119 129 130 sylanbrc J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q ran f s 𝒫 a Fin
132 simplrr J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q X = d
133 uniiun d = q d q
134 simprrr J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q q d q = s f q
135 iuneq2 q d q = s f q q d q = q d s f q
136 134 135 syl J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q q d q = q d s f q
137 133 136 syl5eq J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q d = q d s f q
138 132 137 eqtrd J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q X = q d s f q
139 ssun2 s ran f s
140 vsnid s s
141 139 140 sselii s ran f s
142 elssuni s ran f s s ran f s
143 141 142 ax-mp s ran f s
144 fvssunirn f q ran f
145 ssun1 ran f ran f s
146 145 unissi ran f ran f s
147 144 146 sstri f q ran f s
148 143 147 unssi s f q ran f s
149 148 rgenw q d s f q ran f s
150 iunss q d s f q ran f s q d s f q ran f s
151 149 150 mpbir q d s f q ran f s
152 138 151 eqsstrdi J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q X ran f s
153 31 ad2antrr J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q a J
154 116 153 sstrd J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q ran f J
155 33 ad2antrr J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q s J
156 155 snssd J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q s J
157 154 156 unssd J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q ran f s J
158 uniss ran f s J ran f s J
159 158 1 sseqtrrdi ran f s J ran f s X
160 157 159 syl J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q ran f s X
161 152 160 eqssd J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q X = ran f s
162 unieq b = ran f s b = ran f s
163 162 rspceeqv ran f s 𝒫 a Fin X = ran f s b 𝒫 a Fin X = b
164 131 161 163 syl2anc J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q b 𝒫 a Fin X = b
165 164 expr J Top X = a a J s a x s d ran p a s p X = d d Fin f : d a q d q = s f q b 𝒫 a Fin X = b
166 165 exlimdv J Top X = a a J s a x s d ran p a s p X = d d Fin f f : d a q d q = s f q b 𝒫 a Fin X = b
167 166 ex J Top X = a a J s a x s d ran p a s p X = d d Fin f f : d a q d q = s f q b 𝒫 a Fin X = b
168 113 167 mpdd J Top X = a a J s a x s d ran p a s p X = d d Fin b 𝒫 a Fin X = b
169 87 104 168 3syld J Top X = a a J s a x s d ran p a s p X = d d PtFin b 𝒫 a Fin X = b
170 169 ex J Top X = a a J s a x s d ran p a s p X = d d PtFin b 𝒫 a Fin X = b
171 170 com23 J Top X = a a J s a x s d PtFin d ran p a s p X = d b 𝒫 a Fin X = b
172 171 rexlimdv J Top X = a a J s a x s d PtFin d ran p a s p X = d b 𝒫 a Fin X = b
173 73 172 syld J Top X = a a J s a x s c 𝒫 J X = c d PtFin d c X = d b 𝒫 a Fin X = b
174 173 rexlimdvaa J Top X = a a J s a x s c 𝒫 J X = c d PtFin d c X = d b 𝒫 a Fin X = b
175 30 174 syld J Top X = a a J x X c 𝒫 J X = c d PtFin d c X = d b 𝒫 a Fin X = b
176 175 exlimdv J Top X = a a J x x X c 𝒫 J X = c d PtFin d c X = d b 𝒫 a Fin X = b
177 25 176 syl5bi J Top X = a a J X c 𝒫 J X = c d PtFin d c X = d b 𝒫 a Fin X = b
178 24 177 pm2.61dne J Top X = a a J c 𝒫 J X = c d PtFin d c X = d b 𝒫 a Fin X = b
179 15 178 syl3an3 J Top X = a a 𝒫 J c 𝒫 J X = c d PtFin d c X = d b 𝒫 a Fin X = b
180 179 3exp J Top X = a a 𝒫 J c 𝒫 J X = c d PtFin d c X = d b 𝒫 a Fin X = b
181 180 com24 J Top c 𝒫 J X = c d PtFin d c X = d a 𝒫 J X = a b 𝒫 a Fin X = b
182 181 ralrimdv J Top c 𝒫 J X = c d PtFin d c X = d a 𝒫 J X = a b 𝒫 a Fin X = b
183 1 iscmp J Comp J Top a 𝒫 J X = a b 𝒫 a Fin X = b
184 183 baibr J Top a 𝒫 J X = a b 𝒫 a Fin X = b J Comp
185 182 184 sylibd J Top c 𝒫 J X = c d PtFin d c X = d J Comp
186 14 185 impbid2 J Top J Comp c 𝒫 J X = c d PtFin d c X = d