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 syl5bb ( ( ( 𝑥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 syl5bb ( 𝑢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 syl5bb ( 𝑦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 syl6bi ( ( 𝑦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𝑔RR ) → ( ( 𝑓 <R 𝑔𝑔 <R ) → 𝑓 <R ) )
80 33 79 isso2i <R Or R