Metamath Proof Explorer


Theorem tgcmp

Description: A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub , which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion tgcmp BTopBasesX=BtopGenBCompy𝒫BX=yz𝒫yFinX=z

Proof

Step Hyp Ref Expression
1 eqid topGenB=topGenB
2 1 iscmp topGenBComptopGenBTopy𝒫topGenBtopGenB=yz𝒫yFintopGenB=z
3 2 simprbi topGenBCompy𝒫topGenBtopGenB=yz𝒫yFintopGenB=z
4 unitg BTopBasestopGenB=B
5 eqtr3 topGenB=BX=BtopGenB=X
6 4 5 sylan BTopBasesX=BtopGenB=X
7 6 eqeq1d BTopBasesX=BtopGenB=yX=y
8 6 eqeq1d BTopBasesX=BtopGenB=zX=z
9 8 rexbidv BTopBasesX=Bz𝒫yFintopGenB=zz𝒫yFinX=z
10 7 9 imbi12d BTopBasesX=BtopGenB=yz𝒫yFintopGenB=zX=yz𝒫yFinX=z
11 10 ralbidv BTopBasesX=By𝒫topGenBtopGenB=yz𝒫yFintopGenB=zy𝒫topGenBX=yz𝒫yFinX=z
12 bastg BTopBasesBtopGenB
13 12 adantr BTopBasesX=BBtopGenB
14 13 sspwd BTopBasesX=B𝒫B𝒫topGenB
15 ssralv 𝒫B𝒫topGenBy𝒫topGenBX=yz𝒫yFinX=zy𝒫BX=yz𝒫yFinX=z
16 14 15 syl BTopBasesX=By𝒫topGenBX=yz𝒫yFinX=zy𝒫BX=yz𝒫yFinX=z
17 11 16 sylbid BTopBasesX=By𝒫topGenBtopGenB=yz𝒫yFintopGenB=zy𝒫BX=yz𝒫yFinX=z
18 3 17 syl5 BTopBasesX=BtopGenBCompy𝒫BX=yz𝒫yFinX=z
19 elpwi u𝒫topGenButopGenB
20 simprr BTopBasesX=ButopGenBX=uX=u
21 simprl BTopBasesX=ButopGenBX=uutopGenB
22 21 sselda BTopBasesX=ButopGenBX=ututtopGenB
23 22 adantrr BTopBasesX=ButopGenBX=utuytttopGenB
24 simprr BTopBasesX=ButopGenBX=utuytyt
25 tg2 ttopGenBytwBywwt
26 23 24 25 syl2anc BTopBasesX=ButopGenBX=utuytwBywwt
27 26 expr BTopBasesX=ButopGenBX=utuytwBywwt
28 27 reximdva BTopBasesX=ButopGenBX=utuyttuwBywwt
29 eluni2 yutuyt
30 elunirab ywB|tuwtwBywtuwt
31 r19.42v tuywwtywtuwt
32 31 rexbii wBtuywwtwBywtuwt
33 rexcom wBtuywwttuwBywwt
34 30 32 33 3bitr2i ywB|tuwttuwBywwt
35 28 29 34 3imtr4g BTopBasesX=ButopGenBX=uyuywB|tuwt
36 35 ssrdv BTopBasesX=ButopGenBX=uuwB|tuwt
37 20 36 eqsstrd BTopBasesX=ButopGenBX=uXwB|tuwt
38 ssrab2 wB|tuwtB
39 38 unissi wB|tuwtB
40 simplr BTopBasesX=ButopGenBX=uX=B
41 39 40 sseqtrrid BTopBasesX=ButopGenBX=uwB|tuwtX
42 37 41 eqssd BTopBasesX=ButopGenBX=uX=wB|tuwt
43 elpw2g BTopBaseswB|tuwt𝒫BwB|tuwtB
44 43 ad2antrr BTopBasesX=ButopGenBX=uwB|tuwt𝒫BwB|tuwtB
45 38 44 mpbiri BTopBasesX=ButopGenBX=uwB|tuwt𝒫B
46 unieq y=wB|tuwty=wB|tuwt
47 46 eqeq2d y=wB|tuwtX=yX=wB|tuwt
48 pweq y=wB|tuwt𝒫y=𝒫wB|tuwt
49 48 ineq1d y=wB|tuwt𝒫yFin=𝒫wB|tuwtFin
50 49 rexeqdv y=wB|tuwtz𝒫yFinX=zz𝒫wB|tuwtFinX=z
51 47 50 imbi12d y=wB|tuwtX=yz𝒫yFinX=zX=wB|tuwtz𝒫wB|tuwtFinX=z
52 51 rspcv wB|tuwt𝒫By𝒫BX=yz𝒫yFinX=zX=wB|tuwtz𝒫wB|tuwtFinX=z
53 45 52 syl BTopBasesX=ButopGenBX=uy𝒫BX=yz𝒫yFinX=zX=wB|tuwtz𝒫wB|tuwtFinX=z
54 42 53 mpid BTopBasesX=ButopGenBX=uy𝒫BX=yz𝒫yFinX=zz𝒫wB|tuwtFinX=z
55 elfpw z𝒫wB|tuwtFinzwB|tuwtzFin
56 55 simprbi z𝒫wB|tuwtFinzFin
57 56 ad2antrl BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zzFin
58 55 simplbi z𝒫wB|tuwtFinzwB|tuwt
59 58 ad2antrl BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zzwB|tuwt
60 ssrab zwB|tuwtzBwztuwt
61 60 simprbi zwB|tuwtwztuwt
62 59 61 syl BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zwztuwt
63 sseq2 t=fwwtwfw
64 63 ac6sfi zFinwztuwtff:zuwzwfw
65 57 62 64 syl2anc BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zff:zuwzwfw
66 frn f:zuranfu
67 66 ad2antrl BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zf:zuwzwfwranfu
68 ffn f:zufFnz
69 dffn4 fFnzf:zontoranf
70 68 69 sylib f:zuf:zontoranf
71 70 adantr f:zuwzwfwf:zontoranf
72 fofi zFinf:zontoranfranfFin
73 57 71 72 syl2an BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zf:zuwzwfwranfFin
74 elfpw ranf𝒫uFinranfuranfFin
75 67 73 74 sylanbrc BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zf:zuwzwfwranf𝒫uFin
76 simplrr BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zf:zuwzwfwX=z
77 uniiun z=wzw
78 ss2iun wzwfwwzwwzfw
79 77 78 eqsstrid wzwfwzwzfw
80 79 ad2antll BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zf:zuwzwfwzwzfw
81 fniunfv fFnzwzfw=ranf
82 68 81 syl f:zuwzfw=ranf
83 82 ad2antrl BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zf:zuwzwfwwzfw=ranf
84 80 83 sseqtrd BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zf:zuwzwfwzranf
85 76 84 eqsstrd BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zf:zuwzwfwXranf
86 67 unissd BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zf:zuwzwfwranfu
87 20 ad2antrr BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zf:zuwzwfwX=u
88 86 87 sseqtrrd BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zf:zuwzwfwranfX
89 85 88 eqssd BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zf:zuwzwfwX=ranf
90 unieq v=ranfv=ranf
91 90 rspceeqv ranf𝒫uFinX=ranfv𝒫uFinX=v
92 75 89 91 syl2anc BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zf:zuwzwfwv𝒫uFinX=v
93 65 92 exlimddv BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zv𝒫uFinX=v
94 93 rexlimdvaa BTopBasesX=ButopGenBX=uz𝒫wB|tuwtFinX=zv𝒫uFinX=v
95 54 94 syld BTopBasesX=ButopGenBX=uy𝒫BX=yz𝒫yFinX=zv𝒫uFinX=v
96 95 expr BTopBasesX=ButopGenBX=uy𝒫BX=yz𝒫yFinX=zv𝒫uFinX=v
97 96 com23 BTopBasesX=ButopGenBy𝒫BX=yz𝒫yFinX=zX=uv𝒫uFinX=v
98 19 97 sylan2 BTopBasesX=Bu𝒫topGenBy𝒫BX=yz𝒫yFinX=zX=uv𝒫uFinX=v
99 98 ralrimdva BTopBasesX=By𝒫BX=yz𝒫yFinX=zu𝒫topGenBX=uv𝒫uFinX=v
100 tgcl BTopBasestopGenBTop
101 100 adantr BTopBasesX=BtopGenBTop
102 1 iscmp topGenBComptopGenBTopu𝒫topGenBtopGenB=uv𝒫uFintopGenB=v
103 102 baib topGenBToptopGenBCompu𝒫topGenBtopGenB=uv𝒫uFintopGenB=v
104 101 103 syl BTopBasesX=BtopGenBCompu𝒫topGenBtopGenB=uv𝒫uFintopGenB=v
105 6 eqeq1d BTopBasesX=BtopGenB=uX=u
106 6 eqeq1d BTopBasesX=BtopGenB=vX=v
107 106 rexbidv BTopBasesX=Bv𝒫uFintopGenB=vv𝒫uFinX=v
108 105 107 imbi12d BTopBasesX=BtopGenB=uv𝒫uFintopGenB=vX=uv𝒫uFinX=v
109 108 ralbidv BTopBasesX=Bu𝒫topGenBtopGenB=uv𝒫uFintopGenB=vu𝒫topGenBX=uv𝒫uFinX=v
110 104 109 bitrd BTopBasesX=BtopGenBCompu𝒫topGenBX=uv𝒫uFinX=v
111 99 110 sylibrd BTopBasesX=By𝒫BX=yz𝒫yFinX=ztopGenBComp
112 18 111 impbid BTopBasesX=BtopGenBCompy𝒫BX=yz𝒫yFinX=z