Definition df-enr 5166

Description: Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers df-c 5240, and is intended to be used only by the construction. From Proposition 9-4.1 of [Gleason] p. 126.

Assertion

Ref	Expression
df-enr	|- ~R = {<.x, y>. | ((x e. (P. X. P.) /\ y e. (P. X. P.)) /\ E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ (z +P. u) = (w +P. v)))}

Distinct variable group:   x,y,z,w,v,u

Detailed syntax breakdown of Definition df-enr

Step	Hyp	Ref	Expression
1		cer 4992	. 2 class ~R
2		vx	. . . . . . 7 set x
3	2	cv 955	. . . . . 6 class x
4		cnp 4985	. . . . . . 7 class P.
5	4, 4	cxp 3168	. . . . . 6 class (P. X. P.)
6	3, 5	wcel 958	. . . . 5 wff x e. (P. X. P.)
7		vy	. . . . . . 7 set y
8	7	cv 955	. . . . . 6 class y
9	8, 5	wcel 958	. . . . 5 wff y e. (P. X. P.)
10	6, 9	wa 223	. . . 4 wff (x e. (P. X. P.) /\ y e. (P. X. P.))
11		vz	. . . . . . . . . . . . 13 set z
12	11	cv 955	. . . . . . . . . . . 12 class z
13		vw	. . . . . . . . . . . . 13 set w
14	13	cv 955	. . . . . . . . . . . 12 class w
15	12, 14	cop 2411	. . . . . . . . . . 11 class <.z, w>.
16	3, 15	wceq 956	. . . . . . . . . 10 wff x = <.z, w>.
17		vv	. . . . . . . . . . . . 13 set v
18	17	cv 955	. . . . . . . . . . . 12 class v
19		vu	. . . . . . . . . . . . 13 set u
20	19	cv 955	. . . . . . . . . . . 12 class u
21	18, 20	cop 2411	. . . . . . . . . . 11 class <.v, u>.
22	8, 21	wceq 956	. . . . . . . . . 10 wff y = <.v, u>.
23	16, 22	wa 223	. . . . . . . . 9 wff (x = <.z, w>. /\ y = <.v, u>.)
24		cpp 4987	. . . . . . . . . . 11 class +P.
25	12, 20, 24	co 3963	. . . . . . . . . 10 class (z +P. u)
26	14, 18, 24	co 3963	. . . . . . . . . 10 class (w +P. v)
27	25, 26	wceq 956	. . . . . . . . 9 wff (z +P. u) = (w +P. v)
28	23, 27	wa 223	. . . . . . . 8 wff ((x = <.z, w>. /\ y = <.v, u>.) /\ (z +P. u) = (w +P. v))
29	28, 19	wex 980	. . . . . . 7 wff E.u((x = <.z, w>. /\ y = <.v, u>.) /\ (z +P. u) = (w +P. v))
30	29, 17	wex 980	. . . . . 6 wff E.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ (z +P. u) = (w +P. v))
31	30, 13	wex 980	. . . . 5 wff E.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ (z +P. u) = (w +P. v))
32	31, 11	wex 980	. . . 4 wff E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ (z +P. u) = (w +P. v))
33	10, 32	wa 223	. . 3 wff ((x e. (P. X. P.) /\ y e. (P. X. P.)) /\ E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ (z +P. u) = (w +P. v)))
34	33, 2, 7	copab 2666	. 2 class {<.x, y>. | ((x e. (P. X. P.) /\ y e. (P. X. P.)) /\ E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ (z +P. u) = (w +P. v)))}
35	1, 34	wceq 956	1 wff ~R = {<.x, y>. | ((x e. (P. X. P.) /\ y e. (P. X. P.)) /\ E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ (z +P. u) = (w +P. v)))}

This definition is referenced by:  enrbreq 5174  dmenr 5175  enrer 5176  enrex 5178  addsrpr 5184  mulsrpr 5185

Copyright terms: Public domain