Theorem eltg

Description: Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Assertion	eltg	|- ( B e. V -> ( A e. ( topGen ` B ) <-> A C_ U. ( B i^i ~P A ) ) )

Proof

Step	Hyp	Ref	Expression
1		tgval	|- ( B e. V -> ( topGen ` B ) = { x | x C_ U. ( B i^i ~P x ) } )
2	1	eleq2d	|- ( B e. V -> ( A e. ( topGen ` B ) <-> A e. { x | x C_ U. ( B i^i ~P x ) } ) )
3		elex	|- ( A e. { x | x C_ U. ( B i^i ~P x ) } -> A e. _V )
4	3	adantl	|- ( ( B e. V /\ A e. { x | x C_ U. ( B i^i ~P x ) } ) -> A e. _V )
5		inex1g	|- ( B e. V -> ( B i^i ~P A ) e. _V )
6	5	uniexd	|- ( B e. V -> U. ( B i^i ~P A ) e. _V )
7		ssexg	|- ( ( A C_ U. ( B i^i ~P A ) /\ U. ( B i^i ~P A ) e. _V ) -> A e. _V )
8	6 7	sylan2	|- ( ( A C_ U. ( B i^i ~P A ) /\ B e. V ) -> A e. _V )
9	8	ancoms	|- ( ( B e. V /\ A C_ U. ( B i^i ~P A ) ) -> A e. _V )
10		id	|- ( x = A -> x = A )
11		pweq	|- ( x = A -> ~P x = ~P A )
12	11	ineq2d	|- ( x = A -> ( B i^i ~P x ) = ( B i^i ~P A ) )
13	12	unieqd	|- ( x = A -> U. ( B i^i ~P x ) = U. ( B i^i ~P A ) )
14	10 13	sseq12d	|- ( x = A -> ( x C_ U. ( B i^i ~P x ) <-> A C_ U. ( B i^i ~P A ) ) )
15	14	elabg	|- ( A e. _V -> ( A e. { x | x C_ U. ( B i^i ~P x ) } <-> A C_ U. ( B i^i ~P A ) ) )
16	4 9 15	pm5.21nd	|- ( B e. V -> ( A e. { x | x C_ U. ( B i^i ~P x ) } <-> A C_ U. ( B i^i ~P A ) ) )
17	2 16	bitrd	|- ( B e. V -> ( A e. ( topGen ` B ) <-> A C_ U. ( B i^i ~P A ) ) )