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