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 ) ) )