Definition df-topgen 8864

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 8887). See tgval3 8895 for an alternate expression for the value.

Assertion

Ref	Expression
df-topgen	|- topGen = {<.x, y>. | (x e. Bases /\ y = {z | z C_ U.(x i^i ~Pz)})}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-topgen

Step	Hyp	Ref	Expression
1		ctg 8860	. 2 class topGen
2		vx	. . . . . 6 set x
3	2	cv 1297	. . . . 5 class x
4		ctb 8859	. . . . 5 class Bases
5	3, 4	wcel 1300	. . . 4 wff x e. Bases
6		vy	. . . . . 6 set y
7	6	cv 1297	. . . . 5 class y
8		vz	. . . . . . . 8 set z
9	8	cv 1297	. . . . . . 7 class z
10	9	cpw 3032	. . . . . . . . 9 class ~Pz
11	3, 10	cin 2592	. . . . . . . 8 class (x i^i ~Pz)
12	11	cuni 3177	. . . . . . 7 class U.(x i^i ~Pz)
13	9, 12	wss 2593	. . . . . 6 wff z C_ U.(x i^i ~Pz)
14	13, 8	cab 1871	. . . . 5 class {z | z C_ U.(x i^i ~Pz)}
15	7, 14	wceq 1298	. . . 4 wff y = {z | z C_ U.(x i^i ~Pz)}
16	5, 15	wa 240	. . 3 wff (x e. Bases /\ y = {z | z C_ U.(x i^i ~Pz)})
17	16, 2, 6	copab 3395	. 2 class {<.x, y>. | (x e. Bases /\ y = {z | z C_ U.(x i^i ~Pz)})}
18	1, 17	wceq 1298	1 wff topGen = {<.x, y>. | (x e. Bases /\ y = {z | z C_ U.(x i^i ~Pz)})}

This definition is referenced by:  tgval 8886

Copyright terms: Public domain