| 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
|
syl6bb |
⊢ ( 𝑢 ∈ 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 ∧ 𝑔 ∈ R ∧ ℎ ∈ R ) → ( ( 𝑓 <R 𝑔 ∧ 𝑔 <R ℎ ) → 𝑓 <R ℎ ) ) |
| 80 |
33 79
|
isso2i |
⊢ <R Or R |