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

Metamath Proof Explorer

Definition df-ltr

Description: Define ordering relation on 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.4 of Gleason p. 127. (Contributed by NM, 14-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion df-ltr <R = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ∧ ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) ) ) }

Detailed syntax breakdown

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