This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eltg3

Description: Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006) (Proof shortened by Mario Carneiro, 30-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( A e. ( topGen ` B ) -> B e. dom topGen )
2 inex1g 
 |-  ( B e. dom topGen -> ( B i^i ~P A ) e. _V )
3 1 2 syl 
 |-  ( A e. ( topGen ` B ) -> ( B i^i ~P A ) e. _V )
4 eltg4i 
 |-  ( A e. ( topGen ` B ) -> A = U. ( B i^i ~P A ) )
5 inss1 
 |-  ( B i^i ~P A ) C_ B
6 sseq1 
 |-  ( x = ( B i^i ~P A ) -> ( x C_ B <-> ( B i^i ~P A ) C_ B ) )
7 5 6 mpbiri 
 |-  ( x = ( B i^i ~P A ) -> x C_ B )
8 7 biantrurd 
 |-  ( x = ( B i^i ~P A ) -> ( A = U. x <-> ( x C_ B /\ A = U. x ) ) )
9 unieq 
 |-  ( x = ( B i^i ~P A ) -> U. x = U. ( B i^i ~P A ) )
10 9 eqeq2d 
 |-  ( x = ( B i^i ~P A ) -> ( A = U. x <-> A = U. ( B i^i ~P A ) ) )
11 8 10 bitr3d 
 |-  ( x = ( B i^i ~P A ) -> ( ( x C_ B /\ A = U. x ) <-> A = U. ( B i^i ~P A ) ) )
12 3 4 11 spcedv 
 |-  ( A e. ( topGen ` B ) -> E. x ( x C_ B /\ A = U. x ) )
13 eltg3i 
 |-  ( ( B e. V /\ x C_ B ) -> U. x e. ( topGen ` B ) )
14 eleq1 
 |-  ( A = U. x -> ( A e. ( topGen ` B ) <-> U. x e. ( topGen ` B ) ) )
15 13 14 syl5ibrcom 
 |-  ( ( B e. V /\ x C_ B ) -> ( A = U. x -> A e. ( topGen ` B ) ) )
16 15 expimpd 
 |-  ( B e. V -> ( ( x C_ B /\ A = U. x ) -> A e. ( topGen ` B ) ) )
17 16 exlimdv 
 |-  ( B e. V -> ( E. x ( x C_ B /\ A = U. x ) -> A e. ( topGen ` B ) ) )
18 12 17 impbid2 
 |-  ( B e. V -> ( A e. ( topGen ` B ) <-> E. x ( x C_ B /\ A = U. x ) ) )