Metamath Proof Explorer

Theorem alexsubb

Description: Biconditional form of the Alexander Subbase Theorem alexsub . (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Assertion alexsubb 
|- ( ( X e. UFL /\ X = U. B ) -> ( ( topGen ` ( fi ` B ) ) e. Comp <-> A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. ( topGen ` ( fi ` B ) ) = U. ( topGen ` ( fi ` B ) )
2 1 iscmp 
 |-  ( ( topGen ` ( fi ` B ) ) e. Comp <-> ( ( topGen ` ( fi ` B ) ) e. Top /\ A. x e. ~P ( topGen ` ( fi ` B ) ) ( U. ( topGen ` ( fi ` B ) ) = U. x -> E. y e. ( ~P x i^i Fin ) U. ( topGen ` ( fi ` B ) ) = U. y ) ) )
3 2 simprbi 
 |-  ( ( topGen ` ( fi ` B ) ) e. Comp -> A. x e. ~P ( topGen ` ( fi ` B ) ) ( U. ( topGen ` ( fi ` B ) ) = U. x -> E. y e. ( ~P x i^i Fin ) U. ( topGen ` ( fi ` B ) ) = U. y ) )
4 simpr 
 |-  ( ( X e. UFL /\ X = U. B ) -> X = U. B )
5 elex 
 |-  ( X e. UFL -> X e. _V )
6 5 adantr 
 |-  ( ( X e. UFL /\ X = U. B ) -> X e. _V )
7 4 6 eqeltrrd 
 |-  ( ( X e. UFL /\ X = U. B ) -> U. B e. _V )
8 uniexb 
 |-  ( B e. _V <-> U. B e. _V )
9 7 8 sylibr 
 |-  ( ( X e. UFL /\ X = U. B ) -> B e. _V )
10 fiuni 
 |-  ( B e. _V -> U. B = U. ( fi ` B ) )
11 9 10 syl 
 |-  ( ( X e. UFL /\ X = U. B ) -> U. B = U. ( fi ` B ) )
12 fibas 
 |-  ( fi ` B ) e. TopBases
13 unitg 
 |-  ( ( fi ` B ) e. TopBases -> U. ( topGen ` ( fi ` B ) ) = U. ( fi ` B ) )
14 12 13 mp1i 
 |-  ( ( X e. UFL /\ X = U. B ) -> U. ( topGen ` ( fi ` B ) ) = U. ( fi ` B ) )
15 11 4 14 3eqtr4d 
 |-  ( ( X e. UFL /\ X = U. B ) -> X = U. ( topGen ` ( fi ` B ) ) )
16 15 eqeq1d 
 |-  ( ( X e. UFL /\ X = U. B ) -> ( X = U. x <-> U. ( topGen ` ( fi ` B ) ) = U. x ) )
17 15 eqeq1d 
 |-  ( ( X e. UFL /\ X = U. B ) -> ( X = U. y <-> U. ( topGen ` ( fi ` B ) ) = U. y ) )
18 17 rexbidv 
 |-  ( ( X e. UFL /\ X = U. B ) -> ( E. y e. ( ~P x i^i Fin ) X = U. y <-> E. y e. ( ~P x i^i Fin ) U. ( topGen ` ( fi ` B ) ) = U. y ) )
19 16 18 imbi12d 
 |-  ( ( X e. UFL /\ X = U. B ) -> ( ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) <-> ( U. ( topGen ` ( fi ` B ) ) = U. x -> E. y e. ( ~P x i^i Fin ) U. ( topGen ` ( fi ` B ) ) = U. y ) ) )
20 19 ralbidv 
 |-  ( ( X e. UFL /\ X = U. B ) -> ( A. x e. ~P ( topGen ` ( fi ` B ) ) ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) <-> A. x e. ~P ( topGen ` ( fi ` B ) ) ( U. ( topGen ` ( fi ` B ) ) = U. x -> E. y e. ( ~P x i^i Fin ) U. ( topGen ` ( fi ` B ) ) = U. y ) ) )
21 ssfii 
 |-  ( B e. _V -> B C_ ( fi ` B ) )
22 9 21 syl 
 |-  ( ( X e. UFL /\ X = U. B ) -> B C_ ( fi ` B ) )
23 bastg 
 |-  ( ( fi ` B ) e. TopBases -> ( fi ` B ) C_ ( topGen ` ( fi ` B ) ) )
24 12 23 ax-mp 
 |-  ( fi ` B ) C_ ( topGen ` ( fi ` B ) )
25 22 24 sstrdi 
 |-  ( ( X e. UFL /\ X = U. B ) -> B C_ ( topGen ` ( fi ` B ) ) )
26 25 sspwd 
 |-  ( ( X e. UFL /\ X = U. B ) -> ~P B C_ ~P ( topGen ` ( fi ` B ) ) )
27 ssralv 
 |-  ( ~P B C_ ~P ( topGen ` ( fi ` B ) ) -> ( A. x e. ~P ( topGen ` ( fi ` B ) ) ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) -> A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) )
28 26 27 syl 
 |-  ( ( X e. UFL /\ X = U. B ) -> ( A. x e. ~P ( topGen ` ( fi ` B ) ) ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) -> A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) )
29 20 28 sylbird 
 |-  ( ( X e. UFL /\ X = U. B ) -> ( A. x e. ~P ( topGen ` ( fi ` B ) ) ( U. ( topGen ` ( fi ` B ) ) = U. x -> E. y e. ( ~P x i^i Fin ) U. ( topGen ` ( fi ` B ) ) = U. y ) -> A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) )
30 3 29 syl5 
 |-  ( ( X e. UFL /\ X = U. B ) -> ( ( topGen ` ( fi ` B ) ) e. Comp -> A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) )
31 simpll 
 |-  ( ( ( X e. UFL /\ X = U. B ) /\ A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) -> X e. UFL )
32 simplr 
 |-  ( ( ( X e. UFL /\ X = U. B ) /\ A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) -> X = U. B )
33 eqidd 
 |-  ( ( ( X e. UFL /\ X = U. B ) /\ A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) -> ( topGen ` ( fi ` B ) ) = ( topGen ` ( fi ` B ) ) )
34 velpw 
 |-  ( z e. ~P B <-> z C_ B )
35 unieq 
 |-  ( x = z -> U. x = U. z )
36 35 eqeq2d 
 |-  ( x = z -> ( X = U. x <-> X = U. z ) )
37 pweq 
 |-  ( x = z -> ~P x = ~P z )
38 37 ineq1d 
 |-  ( x = z -> ( ~P x i^i Fin ) = ( ~P z i^i Fin ) )
39 38 rexeqdv 
 |-  ( x = z -> ( E. y e. ( ~P x i^i Fin ) X = U. y <-> E. y e. ( ~P z i^i Fin ) X = U. y ) )
40 36 39 imbi12d 
 |-  ( x = z -> ( ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) <-> ( X = U. z -> E. y e. ( ~P z i^i Fin ) X = U. y ) ) )
41 40 rspccv 
 |-  ( A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) -> ( z e. ~P B -> ( X = U. z -> E. y e. ( ~P z i^i Fin ) X = U. y ) ) )
42 41 adantl 
 |-  ( ( ( X e. UFL /\ X = U. B ) /\ A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) -> ( z e. ~P B -> ( X = U. z -> E. y e. ( ~P z i^i Fin ) X = U. y ) ) )
43 34 42 biimtrrid 
 |-  ( ( ( X e. UFL /\ X = U. B ) /\ A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) -> ( z C_ B -> ( X = U. z -> E. y e. ( ~P z i^i Fin ) X = U. y ) ) )
44 43 imp32 
 |-  ( ( ( ( X e. UFL /\ X = U. B ) /\ A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) /\ ( z C_ B /\ X = U. z ) ) -> E. y e. ( ~P z i^i Fin ) X = U. y )
45 unieq 
 |-  ( y = w -> U. y = U. w )
46 45 eqeq2d 
 |-  ( y = w -> ( X = U. y <-> X = U. w ) )
47 46 cbvrexvw 
 |-  ( E. y e. ( ~P z i^i Fin ) X = U. y <-> E. w e. ( ~P z i^i Fin ) X = U. w )
48 44 47 sylib 
 |-  ( ( ( ( X e. UFL /\ X = U. B ) /\ A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) /\ ( z C_ B /\ X = U. z ) ) -> E. w e. ( ~P z i^i Fin ) X = U. w )
49 31 32 33 48 alexsub 
 |-  ( ( ( X e. UFL /\ X = U. B ) /\ A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) -> ( topGen ` ( fi ` B ) ) e. Comp )
50 49 ex 
 |-  ( ( X e. UFL /\ X = U. B ) -> ( A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) -> ( topGen ` ( fi ` B ) ) e. Comp ) )
51 30 50 impbid 
 |-  ( ( X e. UFL /\ X = U. B ) -> ( ( topGen ` ( fi ` B ) ) e. Comp <-> A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) )