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

Metamath Proof Explorer

Theorem ltsosr

Description: Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion ltsosr <R Or R

Proof

Step Hyp Ref Expression
1 df-nr ⊢ R = ( ( P × P ) / ~R )
2 breq1 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝑓 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ 𝑓 <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) )
3 eqeq1 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝑓 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ 𝑓 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) )
4 breq2 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝑓 → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ↔ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R 𝑓 ) )
5 3 4 orbi12d ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝑓 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∨ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) ↔ ( 𝑓 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∨ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R 𝑓 ) ) )
6 5 notbid ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝑓 → ( ¬ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∨ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) ↔ ¬ ( 𝑓 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∨ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R 𝑓 ) ) )
7 2 6 bibi12d ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝑓 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ ¬ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∨ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) ) ↔ ( 𝑓 <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ ¬ ( 𝑓 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∨ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R 𝑓 ) ) ) )
8 breq2 ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝑔 → ( 𝑓 <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ 𝑓 <R 𝑔 ) )
9 eqeq2 ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝑔 → ( 𝑓 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ 𝑓 = 𝑔 ) )
10 breq1 ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝑔 → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R 𝑓 ↔ 𝑔 <R 𝑓 ) )
11 9 10 orbi12d ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝑔 → ( ( 𝑓 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∨ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R 𝑓 ) ↔ ( 𝑓 = 𝑔 ∨ 𝑔 <R 𝑓 ) ) )
12 11 notbid ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝑔 → ( ¬ ( 𝑓 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∨ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R 𝑓 ) ↔ ¬ ( 𝑓 = 𝑔 ∨ 𝑔 <R 𝑓 ) ) )
13 8 12 bibi12d ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝑔 → ( ( 𝑓 <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ ¬ ( 𝑓 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∨ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R 𝑓 ) ) ↔ ( 𝑓 <R 𝑔 ↔ ¬ ( 𝑓 = 𝑔 ∨ 𝑔 <R 𝑓 ) ) ) )
14 ltsrpr ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ ( 𝑥 +P 𝑤 ) <P ( 𝑦 +P 𝑧 ) )
15 addclpr ⊢ ( ( 𝑥 ∈ P ∧ 𝑤 ∈ P ) → ( 𝑥 +P 𝑤 ) ∈ P )
16 addclpr ⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑦 +P 𝑧 ) ∈ P )
17 ltsopr ⊢ <P Or P
18 sotric ⊢ ( ( <P Or P ∧ ( ( 𝑥 +P 𝑤 ) ∈ P ∧ ( 𝑦 +P 𝑧 ) ∈ P ) ) → ( ( 𝑥 +P 𝑤 ) <P ( 𝑦 +P 𝑧 ) ↔ ¬ ( ( 𝑥 +P 𝑤 ) = ( 𝑦 +P 𝑧 ) ∨ ( 𝑦 +P 𝑧 ) <P ( 𝑥 +P 𝑤 ) ) ) )
19 17 18 mpan ⊢ ( ( ( 𝑥 +P 𝑤 ) ∈ P ∧ ( 𝑦 +P 𝑧 ) ∈ P ) → ( ( 𝑥 +P 𝑤 ) <P ( 𝑦 +P 𝑧 ) ↔ ¬ ( ( 𝑥 +P 𝑤 ) = ( 𝑦 +P 𝑧 ) ∨ ( 𝑦 +P 𝑧 ) <P ( 𝑥 +P 𝑤 ) ) ) )
20 15 16 19 syl2an ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ) → ( ( 𝑥 +P 𝑤 ) <P ( 𝑦 +P 𝑧 ) ↔ ¬ ( ( 𝑥 +P 𝑤 ) = ( 𝑦 +P 𝑧 ) ∨ ( 𝑦 +P 𝑧 ) <P ( 𝑥 +P 𝑤 ) ) ) )
21 20 an42s ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 +P 𝑤 ) <P ( 𝑦 +P 𝑧 ) ↔ ¬ ( ( 𝑥 +P 𝑤 ) = ( 𝑦 +P 𝑧 ) ∨ ( 𝑦 +P 𝑧 ) <P ( 𝑥 +P 𝑤 ) ) ) )
22 enreceq ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ ( 𝑥 +P 𝑤 ) = ( 𝑦 +P 𝑧 ) ) )
23 ltsrpr ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ↔ ( 𝑧 +P 𝑦 ) <P ( 𝑤 +P 𝑥 ) )
24 addcompr ⊢ ( 𝑧 +P 𝑦 ) = ( 𝑦 +P 𝑧 )
25 addcompr ⊢ ( 𝑤 +P 𝑥 ) = ( 𝑥 +P 𝑤 )
26 24 25 breq12i ⊢ ( ( 𝑧 +P 𝑦 ) <P ( 𝑤 +P 𝑥 ) ↔ ( 𝑦 +P 𝑧 ) <P ( 𝑥 +P 𝑤 ) )
27 23 26 bitri ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ↔ ( 𝑦 +P 𝑧 ) <P ( 𝑥 +P 𝑤 ) )
28 27 a1i ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ↔ ( 𝑦 +P 𝑧 ) <P ( 𝑥 +P 𝑤 ) ) )
29 22 28 orbi12d ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∨ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) ↔ ( ( 𝑥 +P 𝑤 ) = ( 𝑦 +P 𝑧 ) ∨ ( 𝑦 +P 𝑧 ) <P ( 𝑥 +P 𝑤 ) ) ) )
30 29 notbid ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ¬ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∨ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) ↔ ¬ ( ( 𝑥 +P 𝑤 ) = ( 𝑦 +P 𝑧 ) ∨ ( 𝑦 +P 𝑧 ) <P ( 𝑥 +P 𝑤 ) ) ) )
31 21 30 bitr4d ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 +P 𝑤 ) <P ( 𝑦 +P 𝑧 ) ↔ ¬ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∨ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) ) )
32 14 31 bitrid ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ ¬ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∨ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) ) )
33 1 7 13 32 2ecoptocl ⊢ ( ( 𝑓 ∈ R ∧ 𝑔 ∈ R ) → ( 𝑓 <R 𝑔 ↔ ¬ ( 𝑓 = 𝑔 ∨ 𝑔 <R 𝑓 ) ) )
34 2 anbi1d ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝑓 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ↔ ( 𝑓 <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ) )
35 breq1 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝑓 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ↔ 𝑓 <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) )
36 34 35 imbi12d ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝑓 → ( ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) → [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ↔ ( ( 𝑓 <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) → 𝑓 <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ) )
37 breq1 ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝑔 → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ↔ 𝑔 <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) )
38 8 37 anbi12d ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝑔 → ( ( 𝑓 <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ↔ ( 𝑓 <R 𝑔 ∧ 𝑔 <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ) )
39 38 imbi1d ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝑔 → ( ( ( 𝑓 <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) → 𝑓 <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ↔ ( ( 𝑓 <R 𝑔 ∧ 𝑔 <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) → 𝑓 <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ) )
40 breq2 ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R = ℎ → ( 𝑔 <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ↔ 𝑔 <R ℎ ) )
41 40 anbi2d ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R = ℎ → ( ( 𝑓 <R 𝑔 ∧ 𝑔 <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ↔ ( 𝑓 <R 𝑔 ∧ 𝑔 <R ℎ ) ) )
42 breq2 ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R = ℎ → ( 𝑓 <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ↔ 𝑓 <R ℎ ) )
43 41 42 imbi12d ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R = ℎ → ( ( ( 𝑓 <R 𝑔 ∧ 𝑔 <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) → 𝑓 <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ↔ ( ( 𝑓 <R 𝑔 ∧ 𝑔 <R ℎ ) → 𝑓 <R ℎ ) ) )
44 ovex ⊢ ( 𝑥 +P 𝑤 ) ∈ V
45 ovex ⊢ ( 𝑦 +P 𝑧 ) ∈ V
46 ltapr ⊢ ( ℎ ∈ P → ( 𝑓 <P 𝑔 ↔ ( ℎ +P 𝑓 ) <P ( ℎ +P 𝑔 ) ) )
47 vex ⊢ 𝑢 ∈ V
48 addcompr ⊢ ( 𝑓 +P 𝑔 ) = ( 𝑔 +P 𝑓 )
49 44 45 46 47 48 caovord2 ⊢ ( 𝑢 ∈ P → ( ( 𝑥 +P 𝑤 ) <P ( 𝑦 +P 𝑧 ) ↔ ( ( 𝑥 +P 𝑤 ) +P 𝑢 ) <P ( ( 𝑦 +P 𝑧 ) +P 𝑢 ) ) )
50 addasspr ⊢ ( ( 𝑥 +P 𝑤 ) +P 𝑢 ) = ( 𝑥 +P ( 𝑤 +P 𝑢 ) )
51 addasspr ⊢ ( ( 𝑦 +P 𝑧 ) +P 𝑢 ) = ( 𝑦 +P ( 𝑧 +P 𝑢 ) )
52 50 51 breq12i ⊢ ( ( ( 𝑥 +P 𝑤 ) +P 𝑢 ) <P ( ( 𝑦 +P 𝑧 ) +P 𝑢 ) ↔ ( 𝑥 +P ( 𝑤 +P 𝑢 ) ) <P ( 𝑦 +P ( 𝑧 +P 𝑢 ) ) )
53 49 52 bitrdi ⊢ ( 𝑢 ∈ P → ( ( 𝑥 +P 𝑤 ) <P ( 𝑦 +P 𝑧 ) ↔ ( 𝑥 +P ( 𝑤 +P 𝑢 ) ) <P ( 𝑦 +P ( 𝑧 +P 𝑢 ) ) ) )
54 14 53 bitrid ⊢ ( 𝑢 ∈ P → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ ( 𝑥 +P ( 𝑤 +P 𝑢 ) ) <P ( 𝑦 +P ( 𝑧 +P 𝑢 ) ) ) )
55 ltsrpr ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ↔ ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) )
56 ltapr ⊢ ( 𝑦 ∈ P → ( ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) ↔ ( 𝑦 +P ( 𝑧 +P 𝑢 ) ) <P ( 𝑦 +P ( 𝑤 +P 𝑣 ) ) ) )
57 55 56 bitrid ⊢ ( 𝑦 ∈ P → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ↔ ( 𝑦 +P ( 𝑧 +P 𝑢 ) ) <P ( 𝑦 +P ( 𝑤 +P 𝑣 ) ) ) )
58 54 57 bi2anan9r ⊢ ( ( 𝑦 ∈ P ∧ 𝑢 ∈ P ) → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ↔ ( ( 𝑥 +P ( 𝑤 +P 𝑢 ) ) <P ( 𝑦 +P ( 𝑧 +P 𝑢 ) ) ∧ ( 𝑦 +P ( 𝑧 +P 𝑢 ) ) <P ( 𝑦 +P ( 𝑤 +P 𝑣 ) ) ) ) )
59 ltrelpr ⊢ <P ⊆ ( P × P )
60 17 59 sotri ⊢ ( ( ( 𝑥 +P ( 𝑤 +P 𝑢 ) ) <P ( 𝑦 +P ( 𝑧 +P 𝑢 ) ) ∧ ( 𝑦 +P ( 𝑧 +P 𝑢 ) ) <P ( 𝑦 +P ( 𝑤 +P 𝑣 ) ) ) → ( 𝑥 +P ( 𝑤 +P 𝑢 ) ) <P ( 𝑦 +P ( 𝑤 +P 𝑣 ) ) )
61 dmplp ⊢ dom +P = ( P × P )
62 0npr ⊢ ¬ ∅ ∈ P
63 ltapr ⊢ ( 𝑤 ∈ P → ( ( 𝑥 +P 𝑢 ) <P ( 𝑦 +P 𝑣 ) ↔ ( 𝑤 +P ( 𝑥 +P 𝑢 ) ) <P ( 𝑤 +P ( 𝑦 +P 𝑣 ) ) ) )
64 61 59 62 63 ndmovordi ⊢ ( ( 𝑤 +P ( 𝑥 +P 𝑢 ) ) <P ( 𝑤 +P ( 𝑦 +P 𝑣 ) ) → ( 𝑥 +P 𝑢 ) <P ( 𝑦 +P 𝑣 ) )
65 vex ⊢ 𝑥 ∈ V
66 vex ⊢ 𝑤 ∈ V
67 addasspr ⊢ ( ( 𝑓 +P 𝑔 ) +P ℎ ) = ( 𝑓 +P ( 𝑔 +P ℎ ) )
68 65 66 47 48 67 caov12 ⊢ ( 𝑥 +P ( 𝑤 +P 𝑢 ) ) = ( 𝑤 +P ( 𝑥 +P 𝑢 ) )
69 vex ⊢ 𝑦 ∈ V
70 vex ⊢ 𝑣 ∈ V
71 69 66 70 48 67 caov12 ⊢ ( 𝑦 +P ( 𝑤 +P 𝑣 ) ) = ( 𝑤 +P ( 𝑦 +P 𝑣 ) )
72 68 71 breq12i ⊢ ( ( 𝑥 +P ( 𝑤 +P 𝑢 ) ) <P ( 𝑦 +P ( 𝑤 +P 𝑣 ) ) ↔ ( 𝑤 +P ( 𝑥 +P 𝑢 ) ) <P ( 𝑤 +P ( 𝑦 +P 𝑣 ) ) )
73 ltsrpr ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ↔ ( 𝑥 +P 𝑢 ) <P ( 𝑦 +P 𝑣 ) )
74 64 72 73 3imtr4i ⊢ ( ( 𝑥 +P ( 𝑤 +P 𝑢 ) ) <P ( 𝑦 +P ( 𝑤 +P 𝑣 ) ) → [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R )
75 60 74 syl ⊢ ( ( ( 𝑥 +P ( 𝑤 +P 𝑢 ) ) <P ( 𝑦 +P ( 𝑧 +P 𝑢 ) ) ∧ ( 𝑦 +P ( 𝑧 +P 𝑢 ) ) <P ( 𝑦 +P ( 𝑤 +P 𝑣 ) ) ) → [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R )
76 58 75 biimtrdi ⊢ ( ( 𝑦 ∈ P ∧ 𝑢 ∈ P ) → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) → [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) )
77 76 ad2ant2l ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) → [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) )
78 77 3adant2 ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) → [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R <R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) )
79 1 36 39 43 78 3ecoptocl ⊢ ( ( 𝑓 ∈ R ∧ 𝑔 ∈ R ∧ ℎ ∈ R ) → ( ( 𝑓 <R 𝑔 ∧ 𝑔 <R ℎ ) → 𝑓 <R ℎ ) )
80 33 79 isso2i ⊢ <R Or R