Metamath Proof Explorer

Theorem tg2

Description: Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006)

Ref Expression
Assertion tg2 
|- ( ( A e. ( topGen ` B ) /\ C e. A ) -> E. x e. B ( C e. x /\ x C_ A ) )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( A e. ( topGen ` B ) -> B e. dom topGen )
2 eltg2b 
 |-  ( B e. dom topGen -> ( A e. ( topGen ` B ) <-> A. y e. A E. x e. B ( y e. x /\ x C_ A ) ) )
3 eleq1 
 |-  ( y = C -> ( y e. x <-> C e. x ) )
4 3 anbi1d 
 |-  ( y = C -> ( ( y e. x /\ x C_ A ) <-> ( C e. x /\ x C_ A ) ) )
5 4 rexbidv 
 |-  ( y = C -> ( E. x e. B ( y e. x /\ x C_ A ) <-> E. x e. B ( C e. x /\ x C_ A ) ) )
6 5 rspccv 
 |-  ( A. y e. A E. x e. B ( y e. x /\ x C_ A ) -> ( C e. A -> E. x e. B ( C e. x /\ x C_ A ) ) )
7 2 6 syl6bi 
 |-  ( B e. dom topGen -> ( A e. ( topGen ` B ) -> ( C e. A -> E. x e. B ( C e. x /\ x C_ A ) ) ) )
8 1 7 mpcom 
 |-  ( A e. ( topGen ` B ) -> ( C e. A -> E. x e. B ( C e. x /\ x C_ A ) ) )
9 8 imp 
 |-  ( ( A e. ( topGen ` B ) /\ C e. A ) -> E. x e. B ( C e. x /\ x C_ A ) )