Definition df-topsp 7595

Description: Define the class of all topological spaces, each of which is an ordered pair the second of which is a topology on the first. See istps5 (future) for a standard way to express a topological space.

Assertion

Ref	Expression
df-topsp	|- TopSp = {<.x, y>. | (y e. Top /\ x = U.y)}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-topsp

Step	Hyp	Ref	Expression
1		ctps 7591	. 2 class TopSp
2		vy	. . . . . 6 set y
3	2	cv 957	. . . . 5 class y
4		ctop 7590	. . . . 5 class Top
5	3, 4	wcel 960	. . . 4 wff y e. Top
6		vx	. . . . . 6 set x
7	6	cv 957	. . . . 5 class x
8	3	cuni 2507	. . . . 5 class U.y
9	7, 8	wceq 958	. . . 4 wff x = U.y
10	5, 9	wa 223	. . 3 wff (y e. Top /\ x = U.y)
11	10, 6, 2	copab 2671	. 2 class {<.x, y>. | (y e. Top /\ x = U.y)}
12	1, 11	wceq 958	1 wff TopSp = {<.x, y>. | (y e. Top /\ x = U.y)}

This definition is referenced by:  eltopsp 7605  tpsex 7606  istps 7607

Copyright terms: Public domain