Definition df-topgen

Description: Define a function that converts a basis to its corresponding topology. Equivalent to the definition of a topology generated by a basis in Munkres p. 78 (see tgval2 ). The first use of this definition is tgval but the token is used in df-pt . See tgval3 for an alternate expression for the value. (Contributed by NM, 16-Jul-2006)

	Ref	Expression
Assertion	df-topgen	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctg	|- topGen
1		vx	|- x
2		cvv	|- _V
3		vy	|- y
4	3	cv	|- y
5	1	cv	|- x
6	4	cpw	|- ~P y
7	5 6	cin	|- ( x i^i ~P y )
8	7	cuni	|- U. ( x i^i ~P y )
9	4 8	wss	|- y C_ U. ( x i^i ~P y )
10	9 3	cab	|- { y | y C_ U. ( x i^i ~P y ) }
11	1 2 10	cmpt	|- ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
12	0 11	wceq	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )