Metamath Proof Explorer

Theorem eltg2

Description: Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

Ref Expression
Assertion eltg2 
|- ( B e. V -> ( A e. ( topGen ` B ) <-> ( A C_ U. B /\ A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) ) )

Proof

Step Hyp Ref Expression
1 tgval2 
 |-  ( B e. V -> ( topGen ` B ) = { z | ( z C_ U. B /\ A. x e. z E. y e. B ( x e. y /\ y C_ z ) ) } )
2 1 eleq2d 
 |-  ( B e. V -> ( A e. ( topGen ` B ) <-> A e. { z | ( z C_ U. B /\ A. x e. z E. y e. B ( x e. y /\ y C_ z ) ) } ) )
3 elex 
 |-  ( A e. { z | ( z C_ U. B /\ A. x e. z E. y e. B ( x e. y /\ y C_ z ) ) } -> A e. _V )
4 3 adantl 
 |-  ( ( B e. V /\ A e. { z | ( z C_ U. B /\ A. x e. z E. y e. B ( x e. y /\ y C_ z ) ) } ) -> A e. _V )
5 uniexg 
 |-  ( B e. V -> U. B e. _V )
6 ssexg 
 |-  ( ( A C_ U. B /\ U. B e. _V ) -> A e. _V )
7 5 6 sylan2 
 |-  ( ( A C_ U. B /\ B e. V ) -> A e. _V )
8 7 ancoms 
 |-  ( ( B e. V /\ A C_ U. B ) -> A e. _V )
9 8 adantrr 
 |-  ( ( B e. V /\ ( A C_ U. B /\ A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) ) -> A e. _V )
10 sseq1 
 |-  ( z = A -> ( z C_ U. B <-> A C_ U. B ) )
11 sseq2 
 |-  ( z = A -> ( y C_ z <-> y C_ A ) )
12 11 anbi2d 
 |-  ( z = A -> ( ( x e. y /\ y C_ z ) <-> ( x e. y /\ y C_ A ) ) )
13 12 rexbidv 
 |-  ( z = A -> ( E. y e. B ( x e. y /\ y C_ z ) <-> E. y e. B ( x e. y /\ y C_ A ) ) )
14 13 raleqbi1dv 
 |-  ( z = A -> ( A. x e. z E. y e. B ( x e. y /\ y C_ z ) <-> A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) )
15 10 14 anbi12d 
 |-  ( z = A -> ( ( z C_ U. B /\ A. x e. z E. y e. B ( x e. y /\ y C_ z ) ) <-> ( A C_ U. B /\ A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) ) )
16 15 elabg 
 |-  ( A e. _V -> ( A e. { z | ( z C_ U. B /\ A. x e. z E. y e. B ( x e. y /\ y C_ z ) ) } <-> ( A C_ U. B /\ A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) ) )
17 4 9 16 pm5.21nd 
 |-  ( B e. V -> ( A e. { z | ( z C_ U. B /\ A. x e. z E. y e. B ( x e. y /\ y C_ z ) ) } <-> ( A C_ U. B /\ A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) ) )
18 2 17 bitrd 
 |-  ( B e. V -> ( A e. ( topGen ` B ) <-> ( A C_ U. B /\ A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) ) )