Definition df-topgen 7574

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 tgval2t 7596). See tgval3t 7604 for an alternate expression for the value.

Assertion

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

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-topgen

Step	Hyp	Ref	Expression
1		ctg 7570	. 2 class topGen
2		vx	. . . . . 6 set x
3	2	cv 954	. . . . 5 class x
4		ctb 7569	. . . . 5 class Bases
5	3, 4	wcel 957	. . . 4 wff x e. Bases
6		vy	. . . . . 6 set y
7	6	cv 954	. . . . 5 class y
8		vz	. . . . . . . 8 set z
9	8	cv 954	. . . . . . 7 class z
10	9	cpw 2399	. . . . . . . . 9 class P~z
11	3, 10	cin 2044	. . . . . . . 8 class (x i^i P~z)
12	11	cuni 2500	. . . . . . 7 class U.(x i^i P~z)
13	9, 12	wss 2045	. . . . . 6 wff z (_ U.(x i^i P~z)
14	13, 8	cab 1463	. . . . 5 class {z | z (_ U.(x i^i P~z)}
15	7, 14	wceq 955	. . . 4 wff y = {z | z (_ U.(x i^i P~z)}
16	5, 15	wa 223	. . 3 wff (x e. Bases /\ y = {z | z (_ U.(x i^i P~z)})
17	16, 2, 6	copab 2663	. 2 class {<.x, y>. | (x e. Bases /\ y = {z | z (_ U.(x i^i P~z)})}
18	1, 17	wceq 955	1 wff topGen = {<.x, y>. | (x e. Bases /\ y = {z | z (_ U.(x i^i P~z)})}

This definition is referenced by:  tgvalt 7595

Copyright terms: Public domain