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