Metamath Proof Explorer

Theorem eltg2b

Description: Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014) (Revised by Mario Carneiro, 10-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 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 ) ) ) )
2 simpl 
 |-  ( ( x e. y /\ y C_ A ) -> x e. y )
3 2 reximi 
 |-  ( E. y e. B ( x e. y /\ y C_ A ) -> E. y e. B x e. y )
4 eluni2 
 |-  ( x e. U. B <-> E. y e. B x e. y )
5 3 4 sylibr 
 |-  ( E. y e. B ( x e. y /\ y C_ A ) -> x e. U. B )
6 5 ralimi 
 |-  ( A. x e. A E. y e. B ( x e. y /\ y C_ A ) -> A. x e. A x e. U. B )
7 dfss3 
 |-  ( A C_ U. B <-> A. x e. A x e. U. B )
8 6 7 sylibr 
 |-  ( A. x e. A E. y e. B ( x e. y /\ y C_ A ) -> A C_ U. B )
9 8 pm4.71ri 
 |-  ( A. x e. A E. y e. B ( x e. y /\ y C_ A ) <-> ( A C_ U. B /\ A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) )
10 1 9 bitr4di 
 |-  ( B e. V -> ( A e. ( topGen ` B ) <-> A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) )