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 = U. J
Assertion alexsubALTlem1
|- ( J e. Comp -> E. x ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )

Proof

Step Hyp Ref Expression
1 alexsubALT.1
 |-  X = U. J
2 cmptop
 |-  ( J e. Comp -> J e. Top )
3 fitop
 |-  ( J e. Top -> ( fi ` J ) = J )
4 3 fveq2d
 |-  ( J e. Top -> ( topGen ` ( fi ` J ) ) = ( topGen ` J ) )
5 tgtop
 |-  ( J e. Top -> ( topGen ` J ) = J )
6 4 5 eqtr2d
 |-  ( J e. Top -> J = ( topGen ` ( fi ` J ) ) )
7 2 6 syl
 |-  ( J e. Comp -> J = ( topGen ` ( fi ` J ) ) )
8 velpw
 |-  ( c e. ~P J <-> c C_ J )
9 1 cmpcov
 |-  ( ( J e. Comp /\ c C_ J /\ X = U. c ) -> E. d e. ( ~P c i^i Fin ) X = U. d )
10 9 3exp
 |-  ( J e. Comp -> ( c C_ J -> ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
11 8 10 syl5bi
 |-  ( J e. Comp -> ( c e. ~P J -> ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
12 11 ralrimiv
 |-  ( J e. Comp -> A. c e. ~P J ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) )
13 2fveq3
 |-  ( x = J -> ( topGen ` ( fi ` x ) ) = ( topGen ` ( fi ` J ) ) )
14 13 eqeq2d
 |-  ( x = J -> ( J = ( topGen ` ( fi ` x ) ) <-> J = ( topGen ` ( fi ` J ) ) ) )
15 pweq
 |-  ( x = J -> ~P x = ~P J )
16 15 raleqdv
 |-  ( x = J -> ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) <-> A. c e. ~P J ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
17 14 16 anbi12d
 |-  ( x = J -> ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) <-> ( J = ( topGen ` ( fi ` J ) ) /\ A. c e. ~P J ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) ) )
18 17 spcegv
 |-  ( J e. Comp -> ( ( J = ( topGen ` ( fi ` J ) ) /\ A. c e. ~P J ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) -> E. x ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) ) )
19 7 12 18 mp2and
 |-  ( J e. Comp -> E. x ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )