Definition df-top 8861

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

Assertion

Ref	Expression
df-top	|- Top = {x | (A.y(y C_ 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 8857	. 2 class Top
2		vy	. . . . . . . 8 set y
3	2	cv 1297	. . . . . . 7 class y
4		vx	. . . . . . . 8 set x
5	4	cv 1297	. . . . . . 7 class x
6	3, 5	wss 2593	. . . . . 6 wff y C_ x
7	3	cuni 3177	. . . . . . 7 class U.y
8	7, 5	wcel 1300	. . . . . 6 wff U.y e. x
9	6, 8	wi 3	. . . . 5 wff (y C_ x -> U.y e. x)
10	9, 2	wal 1296	. . . 4 wff A.y(y C_ x -> U.y e. x)
11		vz	. . . . . . . . 9 set z
12	11	cv 1297	. . . . . . . 8 class z
13	3, 12	cin 2592	. . . . . . 7 class (y i^i z)
14	13, 5	wcel 1300	. . . . . 6 wff (y i^i z) e. x
15	14, 11, 5	wral 2105	. . . . 5 wff A.z e. x (y i^i z) e. x
16	15, 2, 5	wral 2105	. . . 4 wff A.y e. x A.z e. x (y i^i z) e. x
17	10, 16	wa 240	. . 3 wff (A.y(y C_ x -> U.y e. x) /\ A.y e. x A.z e. x (y i^i z) e. x)
18	17, 4	cab 1871	. 2 class {x | (A.y(y C_ x -> U.y e. x) /\ A.y e. x A.z e. x (y i^i z) e. x)}
19	1, 18	wceq 1298	1 wff Top = {x | (A.y(y C_ 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 8865

Copyright terms: Public domain