Theorem tgval

Description: The topology generated by a basis. See also tgval2 and tgval3 . (Contributed by NM, 16-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Assertion	tgval	|- ( B e. V -> ( topGen ` B ) = { x | x C_ U. ( B i^i ~P x ) } )

Proof

Step	Hyp	Ref	Expression
1		df-topgen	|- topGen = ( y e. _V |-> { x | x C_ U. ( y i^i ~P x ) } )
2		ineq1	|- ( y = B -> ( y i^i ~P x ) = ( B i^i ~P x ) )
3	2	unieqd	|- ( y = B -> U. ( y i^i ~P x ) = U. ( B i^i ~P x ) )
4	3	sseq2d	|- ( y = B -> ( x C_ U. ( y i^i ~P x ) <-> x C_ U. ( B i^i ~P x ) ) )
5	4	abbidv	|- ( y = B -> { x | x C_ U. ( y i^i ~P x ) } = { x | x C_ U. ( B i^i ~P x ) } )
6		elex	|- ( B e. V -> B e. _V )
7		uniexg	|- ( B e. V -> U. B e. _V )
8		abssexg	|- ( U. B e. _V -> { x | ( x C_ U. B /\ x C_ U. ~P x ) } e. _V )
9		uniin	|- U. ( B i^i ~P x ) C_ ( U. B i^i U. ~P x )
10		sstr	|- ( ( x C_ U. ( B i^i ~P x ) /\ U. ( B i^i ~P x ) C_ ( U. B i^i U. ~P x ) ) -> x C_ ( U. B i^i U. ~P x ) )
11	9 10	mpan2	|- ( x C_ U. ( B i^i ~P x ) -> x C_ ( U. B i^i U. ~P x ) )
12		ssin	|- ( ( x C_ U. B /\ x C_ U. ~P x ) <-> x C_ ( U. B i^i U. ~P x ) )
13	11 12	sylibr	|- ( x C_ U. ( B i^i ~P x ) -> ( x C_ U. B /\ x C_ U. ~P x ) )
14	13	ss2abi	|- { x | x C_ U. ( B i^i ~P x ) } C_ { x | ( x C_ U. B /\ x C_ U. ~P x ) }
15		ssexg	|- ( ( { x | x C_ U. ( B i^i ~P x ) } C_ { x | ( x C_ U. B /\ x C_ U. ~P x ) } /\ { x | ( x C_ U. B /\ x C_ U. ~P x ) } e. _V ) -> { x | x C_ U. ( B i^i ~P x ) } e. _V )
16	14 15	mpan	|- ( { x | ( x C_ U. B /\ x C_ U. ~P x ) } e. _V -> { x | x C_ U. ( B i^i ~P x ) } e. _V )
17	7 8 16	3syl	|- ( B e. V -> { x | x C_ U. ( B i^i ~P x ) } e. _V )
18	1 5 6 17	fvmptd3	|- ( B e. V -> ( topGen ` B ) = { x | x C_ U. ( B i^i ~P x ) } )