This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( P × P ) ∧ 𝑦 ∈ ( P × P ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 +P 𝑢 ) = ( 𝑤 +P 𝑣 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cer ⊢ ~R
1 vx ⊢ 𝑥
2 vy ⊢ 𝑦
3 1 cv ⊢ 𝑥
4 cnp ⊢ P
5 4 4 cxp ⊢ ( P × P )
6 3 5 wcel ⊢ 𝑥 ∈ ( P × P )
7 2 cv ⊢ 𝑦
8 7 5 wcel ⊢ 𝑦 ∈ ( P × P )
9 6 8 wa ⊢ ( 𝑥 ∈ ( P × P ) ∧ 𝑦 ∈ ( P × P ) )
10 vz ⊢ 𝑧
11 vw ⊢ 𝑤
12 vv ⊢ 𝑣
13 vu ⊢ 𝑢
14 10 cv ⊢ 𝑧
15 11 cv ⊢ 𝑤
16 14 15 cop ⊢ ⟨ 𝑧 , 𝑤 ⟩
17 3 16 wceq ⊢ 𝑥 = ⟨ 𝑧 , 𝑤 ⟩
18 12 cv ⊢ 𝑣
19 13 cv ⊢ 𝑢
20 18 19 cop ⊢ ⟨ 𝑣 , 𝑢 ⟩
21 7 20 wceq ⊢ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩
22 17 21 wa ⊢ ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ )
23 cpp ⊢ +P
24 14 19 23 co ⊢ ( 𝑧 +P 𝑢 )
25 15 18 23 co ⊢ ( 𝑤 +P 𝑣 )
26 24 25 wceq ⊢ ( 𝑧 +P 𝑢 ) = ( 𝑤 +P 𝑣 )
27 22 26 wa ⊢ ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 +P 𝑢 ) = ( 𝑤 +P 𝑣 ) )
28 27 13 wex ⊢ ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 +P 𝑢 ) = ( 𝑤 +P 𝑣 ) )
29 28 12 wex ⊢ ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 +P 𝑢 ) = ( 𝑤 +P 𝑣 ) )
30 29 11 wex ⊢ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 +P 𝑢 ) = ( 𝑤 +P 𝑣 ) )
31 30 10 wex ⊢ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 +P 𝑢 ) = ( 𝑤 +P 𝑣 ) )
32 9 31 wa ⊢ ( ( 𝑥 ∈ ( P × P ) ∧ 𝑦 ∈ ( P × P ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 +P 𝑢 ) = ( 𝑤 +P 𝑣 ) ) )
33 32 1 2 copab ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( P × P ) ∧ 𝑦 ∈ ( P × P ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 +P 𝑢 ) = ( 𝑤 +P 𝑣 ) ) ) }
34 0 33 wceq ⊢ ~R = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( P × P ) ∧ 𝑦 ∈ ( P × P ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 +P 𝑢 ) = ( 𝑤 +P 𝑣 ) ) ) }