Definition df-topgen 16104

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 20760). The first use of this definition is tgval 20759 but the token is used in df-pt 16105. See tgval3 20767 for an alternate expression for the value. (Contributed by NM, 16-Jul-2006.)

Assertion

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

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-topgen

Step	Hyp	Ref	Expression
1		ctg 16098	. 2 class topGen
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		vy	. . . . . 6 setvar y
5	4	cv 1482	. . . . 5 class y
6	2	cv 1482	. . . . . . 7 class x
7	5	cpw 4158	. . . . . . 7 class ~P y
8	6, 7	cin 3573	. . . . . 6 class ( x i^i ~P y )
9	8	cuni 4436	. . . . 5 class U. ( x i^i ~P y )
10	5, 9	wss 3574	. . . 4 wff y C_ U. ( x i^i ~P y )
11	10, 4	cab 2608	. . 3 class { y | y C_ U. ( x i^i ~P y ) }
12	2, 3, 11	cmpt 4729	. 2 class ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
13	1, 12	wceq 1483	1 wff topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )

This definition is referenced by:  tgval  20759