Metamath Proof Explorer

Definition df-enr

Description: Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers df-c , 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.)

Ref Expression
Assertion 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 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cer 
 |-  ~R
1 vx 
 |-  x
2 vy 
 |-  y
3 1 cv 
 |-  x
4 cnp 
 |-  P.
5 4 4 cxp 
 |-  ( P. X. P. )
6 3 5 wcel 
 |-  x e. ( P. X. P. )
7 2 cv 
 |-  y
8 7 5 wcel 
 |-  y e. ( P. X. P. )
9 6 8 wa 
 |-  ( x e. ( P. X. P. ) /\ y e. ( P. X. P. ) )
10 vz 
 |-  z
11 vw 
 |-  w
12 vv 
 |-  v
13 vu 
 |-  u
14 10 cv 
 |-  z
15 11 cv 
 |-  w
16 14 15 cop 
 |-  <. z , w >.
17 3 16 wceq 
 |-  x = <. z , w >.
18 12 cv 
 |-  v
19 13 cv 
 |-  u
20 18 19 cop 
 |-  <. v , u >.
21 7 20 wceq 
 |-  y = <. v , u >.
22 17 21 wa 
 |-  ( x = <. z , w >. /\ y = <. v , u >. )
23 cpp 
 |-  +P.
24 14 19 23 co 
 |-  ( z +P. u )
25 15 18 23 co 
 |-  ( w +P. v )
26 24 25 wceq 
 |-  ( z +P. u ) = ( w +P. v )
27 22 26 wa 
 |-  ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) )
28 27 13 wex 
 |-  E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) )
29 28 12 wex 
 |-  E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) )
30 29 11 wex 
 |-  E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) )
31 30 10 wex 
 |-  E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) )
32 9 31 wa 
 |-  ( ( 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 ) ) )
33 32 1 2 copab 
 |-  { <. 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 ) ) ) }
34 0 33 wceq 
 |-  ~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 ) ) ) }