Definition df-enr 9877

Description: Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9942, and is intended to be used only by the construction. From Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.)

Assertion

Ref	Expression
df-enr	|- ~R = { <. x , y >. | ( ( x e. ( P. X. P. ) /\ y e. ( P. X. P. ) ) /\ E. z E. w E. v E. 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 9686	. 2 class ~R
2		vx	. . . . . . 7 setvar x
3	2	cv 1482	. . . . . 6 class x
4		cnp 9681	. . . . . . 7 class P.
5	4, 4	cxp 5112	. . . . . 6 class ( P. X. P. )
6	3, 5	wcel 1990	. . . . 5 wff x e. ( P. X. P. )
7		vy	. . . . . . 7 setvar y
8	7	cv 1482	. . . . . 6 class y
9	8, 5	wcel 1990	. . . . 5 wff y e. ( P. X. P. )
10	6, 9	wa 384	. . . 4 wff ( x e. ( P. X. P. ) /\ y e. ( P. X. P. ) )
11		vz	. . . . . . . . . . . . 13 setvar z
12	11	cv 1482	. . . . . . . . . . . 12 class z
13		vw	. . . . . . . . . . . . 13 setvar w
14	13	cv 1482	. . . . . . . . . . . 12 class w
15	12, 14	cop 4183	. . . . . . . . . . 11 class <. z , w >.
16	3, 15	wceq 1483	. . . . . . . . . 10 wff x = <. z , w >.
17		vv	. . . . . . . . . . . . 13 setvar v
18	17	cv 1482	. . . . . . . . . . . 12 class v
19		vu	. . . . . . . . . . . . 13 setvar u
20	19	cv 1482	. . . . . . . . . . . 12 class u
21	18, 20	cop 4183	. . . . . . . . . . 11 class <. v , u >.
22	8, 21	wceq 1483	. . . . . . . . . 10 wff y = <. v , u >.
23	16, 22	wa 384	. . . . . . . . 9 wff ( x = <. z , w >. /\ y = <. v , u >. )
24		cpp 9683	. . . . . . . . . . 11 class +P.
25	12, 20, 24	co 6650	. . . . . . . . . 10 class ( z +P. u )
26	14, 18, 24	co 6650	. . . . . . . . . 10 class ( w +P. v )
27	25, 26	wceq 1483	. . . . . . . . 9 wff ( z +P. u ) = ( w +P. v )
28	23, 27	wa 384	. . . . . . . 8 wff ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) )
29	28, 19	wex 1704	. . . . . . 7 wff E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) )
30	29, 17	wex 1704	. . . . . 6 wff E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) )
31	30, 13	wex 1704	. . . . 5 wff E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) )
32	31, 11	wex 1704	. . . 4 wff E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) )
33	10, 32	wa 384	. . 3 wff ( ( x e. ( P. X. P. ) /\ y e. ( P. X. P. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) ) )
34	33, 2, 7	copab 4712	. 2 class { <. x , y >. | ( ( x e. ( P. X. P. ) /\ y e. ( P. X. P. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) ) ) }
35	1, 34	wceq 1483	1 wff ~R = { <. x , y >. | ( ( x e. ( P. X. P. ) /\ y e. ( P. X. P. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) ) ) }

This definition is referenced by:  enrbreq  9885  enrer  9886  enrex  9888  prsrlem1  9893