Theorem bastg

Description: A member of a basis is a subset of the topology it generates. (Contributed by NM, 16-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Assertion	bastg	|- ( B e. V -> B C_ ( topGen ` B ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( B e. V /\ x e. B ) -> x e. B )
2		vex	|- x e. _V
3	2	pwid	|- x e. ~P x
4	3	a1i	|- ( ( B e. V /\ x e. B ) -> x e. ~P x )
5	1 4	elind	|- ( ( B e. V /\ x e. B ) -> x e. ( B i^i ~P x ) )
6		elssuni	|- ( x e. ( B i^i ~P x ) -> x C_ U. ( B i^i ~P x ) )
7	5 6	syl	|- ( ( B e. V /\ x e. B ) -> x C_ U. ( B i^i ~P x ) )
8	7	ex	|- ( B e. V -> ( x e. B -> x C_ U. ( B i^i ~P x ) ) )
9		eltg	|- ( B e. V -> ( x e. ( topGen ` B ) <-> x C_ U. ( B i^i ~P x ) ) )
10	8 9	sylibrd	|- ( B e. V -> ( x e. B -> x e. ( topGen ` B ) ) )
11	10	ssrdv	|- ( B e. V -> B C_ ( topGen ` B ) )