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 ⊢ ~ 𝑹 = x y | x ∈ 𝑷 × 𝑷 ∧ y ∈ 𝑷 × 𝑷 ∧ ∃ z ∃ w ∃ v ∃ u x = z w ∧ y = v u ∧ z + 𝑷 u = w + 𝑷 v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cer class ~ 𝑹
1 vx setvar x
2 vy setvar y
3 1 cv setvar x
4 cnp class 𝑷
5 4 4 cxp class 𝑷 × 𝑷
6 3 5 wcel wff x ∈ 𝑷 × 𝑷
7 2 cv setvar y
8 7 5 wcel wff y ∈ 𝑷 × 𝑷
9 6 8 wa wff x ∈ 𝑷 × 𝑷 ∧ y ∈ 𝑷 × 𝑷
10 vz setvar z
11 vw setvar w
12 vv setvar v
13 vu setvar u
14 10 cv setvar z
15 11 cv setvar w
16 14 15 cop class z w
17 3 16 wceq wff x = z w
18 12 cv setvar v
19 13 cv setvar u
20 18 19 cop class v u
21 7 20 wceq wff y = v u
22 17 21 wa wff x = z w ∧ y = v u
23 cpp class + 𝑷
24 14 19 23 co class z + 𝑷 u
25 15 18 23 co class w + 𝑷 v
26 24 25 wceq wff z + 𝑷 u = w + 𝑷 v
27 22 26 wa wff x = z w ∧ y = v u ∧ z + 𝑷 u = w + 𝑷 v
28 27 13 wex wff ∃ u x = z w ∧ y = v u ∧ z + 𝑷 u = w + 𝑷 v
29 28 12 wex wff ∃ v ∃ u x = z w ∧ y = v u ∧ z + 𝑷 u = w + 𝑷 v
30 29 11 wex wff ∃ w ∃ v ∃ u x = z w ∧ y = v u ∧ z + 𝑷 u = w + 𝑷 v
31 30 10 wex wff ∃ z ∃ w ∃ v ∃ u x = z w ∧ y = v u ∧ z + 𝑷 u = w + 𝑷 v
32 9 31 wa wff x ∈ 𝑷 × 𝑷 ∧ y ∈ 𝑷 × 𝑷 ∧ ∃ z ∃ w ∃ v ∃ u x = z w ∧ y = v u ∧ z + 𝑷 u = w + 𝑷 v
33 32 1 2 copab class x y | x ∈ 𝑷 × 𝑷 ∧ y ∈ 𝑷 × 𝑷 ∧ ∃ z ∃ w ∃ v ∃ u x = z w ∧ y = v u ∧ z + 𝑷 u = w + 𝑷 v
34 0 33 wceq wff ~ 𝑹 = x y | x ∈ 𝑷 × 𝑷 ∧ y ∈ 𝑷 × 𝑷 ∧ ∃ z ∃ w ∃ v ∃ u x = z w ∧ y = v u ∧ z + 𝑷 u = w + 𝑷 v