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