Definition df-subsp 10553

Description: Function returning the subspace topology induced by the topology y and the set x.

Assertion

Ref	Expression
df-subsp	|- subSp = {<.<.x, y>., z>. | (y e. Top /\ z = {u | E.v e. y u = (v i^i x)})}

Distinct variable groups:   x,y,z,u   x,v,y,z

Detailed syntax breakdown of Definition df-subsp

Step	Hyp	Ref	Expression
1		csubsp 10552	. 2 class subSp
2		vy	. . . . . 6 set y
3	2	cv 955	. . . . 5 class y
4		ctop 7588	. . . . 5 class Top
5	3, 4	wcel 958	. . . 4 wff y e. Top
6		vz	. . . . . 6 set z
7	6	cv 955	. . . . 5 class z
8		vu	. . . . . . . . 9 set u
9	8	cv 955	. . . . . . . 8 class u
10		vv	. . . . . . . . . 10 set v
11	10	cv 955	. . . . . . . . 9 class v
12		vx	. . . . . . . . . 10 set x
13	12	cv 955	. . . . . . . . 9 class x
14	11, 13	cin 2046	. . . . . . . 8 class (v i^i x)
15	9, 14	wceq 956	. . . . . . 7 wff u = (v i^i x)
16	15, 10, 3	wrex 1646	. . . . . 6 wff E.v e. y u = (v i^i x)
17	16, 8	cab 1463	. . . . 5 class {u | E.v e. y u = (v i^i x)}
18	7, 17	wceq 956	. . . 4 wff z = {u | E.v e. y u = (v i^i x)}
19	5, 18	wa 223	. . 3 wff (y e. Top /\ z = {u | E.v e. y u = (v i^i x)})
20	19, 12, 2, 6	copab2 3964	. 2 class {<.<.x, y>., z>. | (y e. Top /\ z = {u | E.v e. y u = (v i^i x)})}
21	1, 20	wceq 956	1 wff subSp = {<.<.x, y>., z>. | (y e. Top /\ z = {u | E.v e. y u = (v i^i x)})}

This definition is referenced by:  subsp 10554

Copyright terms: Public domain