Metamath Proof Explorer


Theorem alexsubALTlem1

Description: Lemma for alexsubALT . A compact space has a subbase such that every cover taken from it has a finite subcover. (Contributed by Jeff Hankins, 27-Jan-2010)

Ref Expression
Hypothesis alexsubALT.1 X=J
Assertion alexsubALTlem1 JCompxJ=topGenfixc𝒫xX=cd𝒫cFinX=d

Proof

Step Hyp Ref Expression
1 alexsubALT.1 X=J
2 cmptop JCompJTop
3 fitop JTopfiJ=J
4 3 fveq2d JToptopGenfiJ=topGenJ
5 tgtop JToptopGenJ=J
6 4 5 eqtr2d JTopJ=topGenfiJ
7 2 6 syl JCompJ=topGenfiJ
8 velpw c𝒫JcJ
9 1 cmpcov JCompcJX=cd𝒫cFinX=d
10 9 3exp JCompcJX=cd𝒫cFinX=d
11 8 10 syl5bi JCompc𝒫JX=cd𝒫cFinX=d
12 11 ralrimiv JCompc𝒫JX=cd𝒫cFinX=d
13 2fveq3 x=JtopGenfix=topGenfiJ
14 13 eqeq2d x=JJ=topGenfixJ=topGenfiJ
15 pweq x=J𝒫x=𝒫J
16 15 raleqdv x=Jc𝒫xX=cd𝒫cFinX=dc𝒫JX=cd𝒫cFinX=d
17 14 16 anbi12d x=JJ=topGenfixc𝒫xX=cd𝒫cFinX=dJ=topGenfiJc𝒫JX=cd𝒫cFinX=d
18 17 spcegv JCompJ=topGenfiJc𝒫JX=cd𝒫cFinX=dxJ=topGenfixc𝒫xX=cd𝒫cFinX=d
19 7 12 18 mp2and JCompxJ=topGenfixc𝒫xX=cd𝒫cFinX=d