Definition df-hmph 10523

Description: Definition of the relation x is homeomorph to y.

Assertion

Ref	Expression
df-hmph	|- ~= = {<.x, y>. | (x e. Top /\ y e. Top /\ E.f f e. (x Homeo y))}

Distinct variable group:   x,y,f

Detailed syntax breakdown of Definition df-hmph

Step	Hyp	Ref	Expression
1		chomeo 10514	. 2 class ~=
2		vx	. . . . . 6 set x
3	2	cv 955	. . . . 5 class x
4		ctop 7588	. . . . 5 class Top
5	3, 4	wcel 958	. . . 4 wff x e. Top
6		vy	. . . . . 6 set y
7	6	cv 955	. . . . 5 class y
8	7, 4	wcel 958	. . . 4 wff y e. Top
9		vf	. . . . . . 7 set f
10	9	cv 955	. . . . . 6 class f
11		chomeosm 10513	. . . . . . 7 class Homeo
12	3, 7, 11	co 3963	. . . . . 6 class (x Homeo y)
13	10, 12	wcel 958	. . . . 5 wff f e. (x Homeo y)
14	13, 9	wex 980	. . . 4 wff E.f f e. (x Homeo y)
15	5, 8, 14	w3a 775	. . 3 wff (x e. Top /\ y e. Top /\ E.f f e. (x Homeo y))
16	15, 2, 6	copab 2666	. 2 class {<.x, y>. | (x e. Top /\ y e. Top /\ E.f f e. (x Homeo y))}
17	1, 16	wceq 956	1 wff ~= = {<.x, y>. | (x e. Top /\ y e. Top /\ E.f f e. (x Homeo y))}

This definition is referenced by:  hmph 10524  dmhmph 10532  rnhmph 10533

Copyright terms: Public domain