Definition df-top 7552

Description: Define the (proper) class of all topologies. See istop2g 7557 for an alternate way to express finite intersection and istps5 7570 for a standard definition in terms of both members of a topological space.

Assertion

Ref	Expression
df-top	|- Top = {x | (A.y(y (_ x -> U.y e. x) /\ A.y e. x A.z e. x (y i^i z) e. x)}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-top

Step	Hyp	Ref	Expression
1		ctop 7548	. 2 class Top
2		vy	. . . . . . . 8 set y
3	2	cv 954	. . . . . . 7 class y
4		vx	. . . . . . . 8 set x
5	4	cv 954	. . . . . . 7 class x
6	3, 5	wss 2044	. . . . . 6 wff y (_ x
7	3	cuni 2499	. . . . . . 7 class U.y
8	7, 5	wcel 957	. . . . . 6 wff U.y e. x
9	6, 8	wi 3	. . . . 5 wff (y (_ x -> U.y e. x)
10	9, 2	wal 953	. . . 4 wff A.y(y (_ x -> U.y e. x)
11		vz	. . . . . . . . 9 set z
12	11	cv 954	. . . . . . . 8 class z
13	3, 12	cin 2043	. . . . . . 7 class (y i^i z)
14	13, 5	wcel 957	. . . . . 6 wff (y i^i z) e. x
15	14, 11, 5	wral 1643	. . . . 5 wff A.z e. x (y i^i z) e. x
16	15, 2, 5	wral 1643	. . . 4 wff A.y e. x A.z e. x (y i^i z) e. x
17	10, 16	wa 223	. . 3 wff (A.y(y (_ x -> U.y e. x) /\ A.y e. x A.z e. x (y i^i z) e. x)
18	17, 4	cab 1462	. 2 class {x | (A.y(y (_ x -> U.y e. x) /\ A.y e. x A.z e. x (y i^i z) e. x)}
19	1, 18	wceq 955	1 wff Top = {x | (A.y(y (_ x -> U.y e. x) /\ A.y e. x A.z e. x (y i^i z) e. x)}

This definition is referenced by:  istopg 7556

Copyright terms: Public domain