| Step | Hyp | Ref
| Expression |
| 1 | | enrer 11103 |
. . 3
⊢
~R Er (P ×
P) |
| 2 | | erdm 8755 |
. . 3
⊢ (
~R Er (P × P) →
dom ~R = (P ×
P)) |
| 3 | 1, 2 | ax-mp 5 |
. 2
⊢ dom
~R = (P ×
P) |
| 4 | | df-nr 11096 |
. 2
⊢
R = ((P × P) /
~R ) |
| 5 | | ltrelsr 11108 |
. 2
⊢
<R ⊆ (R ×
R) |
| 6 | | ltrelpr 11038 |
. 2
⊢
<P ⊆ (P ×
P) |
| 7 | | 0npr 11032 |
. 2
⊢ ¬
∅ ∈ P |
| 8 | | dmplp 11052 |
. 2
⊢ dom
+P = (P ×
P) |
| 9 | | enrex 11107 |
. . 3
⊢
~R ∈ V |
| 10 | | df-ltr 11099 |
. . 3
⊢
<R = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧
∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ~R ∧
𝑦 = [〈𝑣, 𝑢〉] ~R ) ∧
(𝑧
+P 𝑢)<P (𝑤 +P
𝑣)))} |
| 11 | | addclpr 11058 |
. . . . . . 7
⊢ ((𝑤 ∈ P ∧
𝑣 ∈ P)
→ (𝑤
+P 𝑣) ∈ P) |
| 12 | 11 | ad2ant2lr 748 |
. . . . . 6
⊢ (((𝑧 ∈ P ∧
𝑤 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → (𝑤 +P 𝑣) ∈
P) |
| 13 | | addclpr 11058 |
. . . . . . 7
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝐵
+P 𝐶) ∈ P) |
| 14 | 13 | ad2ant2lr 748 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝐶 ∈
P ∧ 𝐷
∈ P)) → (𝐵 +P 𝐶) ∈
P) |
| 15 | 12, 14 | anim12ci 614 |
. . . . 5
⊢ ((((𝑧 ∈ P ∧
𝑤 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) ∧ ((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧
(𝐶 ∈ P
∧ 𝐷 ∈
P))) → ((𝐵 +P 𝐶) ∈ P ∧
(𝑤
+P 𝑣) ∈ P)) |
| 16 | 15 | an4s 660 |
. . . 4
⊢ ((((𝑧 ∈ P ∧
𝑤 ∈ P)
∧ (𝐴 ∈
P ∧ 𝐵
∈ P)) ∧ ((𝑣 ∈ P ∧ 𝑢 ∈ P) ∧
(𝐶 ∈ P
∧ 𝐷 ∈
P))) → ((𝐵 +P 𝐶) ∈ P ∧
(𝑤
+P 𝑣) ∈ P)) |
| 17 | | enreceq 11106 |
. . . . . 6
⊢ (((𝑧 ∈ P ∧
𝑤 ∈ P)
∧ (𝐴 ∈
P ∧ 𝐵
∈ P)) → ([〈𝑧, 𝑤〉] ~R =
[〈𝐴, 𝐵〉] ~R ↔
(𝑧
+P 𝐵) = (𝑤 +P 𝐴))) |
| 18 | | enreceq 11106 |
. . . . . . 7
⊢ (((𝑣 ∈ P ∧
𝑢 ∈ P)
∧ (𝐶 ∈
P ∧ 𝐷
∈ P)) → ([〈𝑣, 𝑢〉] ~R =
[〈𝐶, 𝐷〉] ~R ↔
(𝑣
+P 𝐷) = (𝑢 +P 𝐶))) |
| 19 | | eqcom 2744 |
. . . . . . 7
⊢ ((𝑣 +P
𝐷) = (𝑢 +P 𝐶) ↔ (𝑢 +P 𝐶) = (𝑣 +P 𝐷)) |
| 20 | 18, 19 | bitrdi 287 |
. . . . . 6
⊢ (((𝑣 ∈ P ∧
𝑢 ∈ P)
∧ (𝐶 ∈
P ∧ 𝐷
∈ P)) → ([〈𝑣, 𝑢〉] ~R =
[〈𝐶, 𝐷〉] ~R ↔
(𝑢
+P 𝐶) = (𝑣 +P 𝐷))) |
| 21 | 17, 20 | bi2anan9 638 |
. . . . 5
⊢ ((((𝑧 ∈ P ∧
𝑤 ∈ P)
∧ (𝐴 ∈
P ∧ 𝐵
∈ P)) ∧ ((𝑣 ∈ P ∧ 𝑢 ∈ P) ∧
(𝐶 ∈ P
∧ 𝐷 ∈
P))) → (([〈𝑧, 𝑤〉] ~R =
[〈𝐴, 𝐵〉] ~R ∧
[〈𝑣, 𝑢〉]
~R = [〈𝐶, 𝐷〉] ~R ) ↔
((𝑧
+P 𝐵) = (𝑤 +P 𝐴) ∧ (𝑢 +P 𝐶) = (𝑣 +P 𝐷)))) |
| 22 | | oveq12 7440 |
. . . . . 6
⊢ (((𝑧 +P
𝐵) = (𝑤 +P 𝐴) ∧ (𝑢 +P 𝐶) = (𝑣 +P 𝐷)) → ((𝑧 +P 𝐵) +P
(𝑢
+P 𝐶)) = ((𝑤 +P 𝐴) +P
(𝑣
+P 𝐷))) |
| 23 | | addcompr 11061 |
. . . . . . . . . 10
⊢ (𝑢 +P
𝐵) = (𝐵 +P 𝑢) |
| 24 | 23 | oveq1i 7441 |
. . . . . . . . 9
⊢ ((𝑢 +P
𝐵)
+P 𝐶) = ((𝐵 +P 𝑢) +P
𝐶) |
| 25 | | addasspr 11062 |
. . . . . . . . 9
⊢ ((𝑢 +P
𝐵)
+P 𝐶) = (𝑢 +P (𝐵 +P
𝐶)) |
| 26 | | addasspr 11062 |
. . . . . . . . 9
⊢ ((𝐵 +P
𝑢)
+P 𝐶) = (𝐵 +P (𝑢 +P
𝐶)) |
| 27 | 24, 25, 26 | 3eqtr3i 2773 |
. . . . . . . 8
⊢ (𝑢 +P
(𝐵
+P 𝐶)) = (𝐵 +P (𝑢 +P
𝐶)) |
| 28 | 27 | oveq2i 7442 |
. . . . . . 7
⊢ (𝑧 +P
(𝑢
+P (𝐵 +P 𝐶))) = (𝑧 +P (𝐵 +P
(𝑢
+P 𝐶))) |
| 29 | | addasspr 11062 |
. . . . . . 7
⊢ ((𝑧 +P
𝑢)
+P (𝐵 +P 𝐶)) = (𝑧 +P (𝑢 +P
(𝐵
+P 𝐶))) |
| 30 | | addasspr 11062 |
. . . . . . 7
⊢ ((𝑧 +P
𝐵)
+P (𝑢 +P 𝐶)) = (𝑧 +P (𝐵 +P
(𝑢
+P 𝐶))) |
| 31 | 28, 29, 30 | 3eqtr4i 2775 |
. . . . . 6
⊢ ((𝑧 +P
𝑢)
+P (𝐵 +P 𝐶)) = ((𝑧 +P 𝐵) +P
(𝑢
+P 𝐶)) |
| 32 | | addcompr 11061 |
. . . . . . . . . 10
⊢ (𝑣 +P
𝐴) = (𝐴 +P 𝑣) |
| 33 | 32 | oveq1i 7441 |
. . . . . . . . 9
⊢ ((𝑣 +P
𝐴)
+P 𝐷) = ((𝐴 +P 𝑣) +P
𝐷) |
| 34 | | addasspr 11062 |
. . . . . . . . 9
⊢ ((𝑣 +P
𝐴)
+P 𝐷) = (𝑣 +P (𝐴 +P
𝐷)) |
| 35 | | addasspr 11062 |
. . . . . . . . 9
⊢ ((𝐴 +P
𝑣)
+P 𝐷) = (𝐴 +P (𝑣 +P
𝐷)) |
| 36 | 33, 34, 35 | 3eqtr3i 2773 |
. . . . . . . 8
⊢ (𝑣 +P
(𝐴
+P 𝐷)) = (𝐴 +P (𝑣 +P
𝐷)) |
| 37 | 36 | oveq2i 7442 |
. . . . . . 7
⊢ (𝑤 +P
(𝑣
+P (𝐴 +P 𝐷))) = (𝑤 +P (𝐴 +P
(𝑣
+P 𝐷))) |
| 38 | | addasspr 11062 |
. . . . . . 7
⊢ ((𝑤 +P
𝑣)
+P (𝐴 +P 𝐷)) = (𝑤 +P (𝑣 +P
(𝐴
+P 𝐷))) |
| 39 | | addasspr 11062 |
. . . . . . 7
⊢ ((𝑤 +P
𝐴)
+P (𝑣 +P 𝐷)) = (𝑤 +P (𝐴 +P
(𝑣
+P 𝐷))) |
| 40 | 37, 38, 39 | 3eqtr4i 2775 |
. . . . . 6
⊢ ((𝑤 +P
𝑣)
+P (𝐴 +P 𝐷)) = ((𝑤 +P 𝐴) +P
(𝑣
+P 𝐷)) |
| 41 | 22, 31, 40 | 3eqtr4g 2802 |
. . . . 5
⊢ (((𝑧 +P
𝐵) = (𝑤 +P 𝐴) ∧ (𝑢 +P 𝐶) = (𝑣 +P 𝐷)) → ((𝑧 +P 𝑢) +P
(𝐵
+P 𝐶)) = ((𝑤 +P 𝑣) +P
(𝐴
+P 𝐷))) |
| 42 | 21, 41 | biimtrdi 253 |
. . . 4
⊢ ((((𝑧 ∈ P ∧
𝑤 ∈ P)
∧ (𝐴 ∈
P ∧ 𝐵
∈ P)) ∧ ((𝑣 ∈ P ∧ 𝑢 ∈ P) ∧
(𝐶 ∈ P
∧ 𝐷 ∈
P))) → (([〈𝑧, 𝑤〉] ~R =
[〈𝐴, 𝐵〉] ~R ∧
[〈𝑣, 𝑢〉]
~R = [〈𝐶, 𝐷〉] ~R ) →
((𝑧
+P 𝑢) +P (𝐵 +P
𝐶)) = ((𝑤 +P 𝑣) +P
(𝐴
+P 𝐷)))) |
| 43 | | ovex 7464 |
. . . . 5
⊢ (𝑧 +P
𝑢) ∈
V |
| 44 | | ovex 7464 |
. . . . 5
⊢ (𝐵 +P
𝐶) ∈
V |
| 45 | | ltapr 11085 |
. . . . 5
⊢ (𝑓 ∈ P →
(𝑥<P 𝑦 ↔ (𝑓 +P 𝑥)<P
(𝑓
+P 𝑦))) |
| 46 | | ovex 7464 |
. . . . 5
⊢ (𝑤 +P
𝑣) ∈
V |
| 47 | | addcompr 11061 |
. . . . 5
⊢ (𝑥 +P
𝑦) = (𝑦 +P 𝑥) |
| 48 | | ovex 7464 |
. . . . 5
⊢ (𝐴 +P
𝐷) ∈
V |
| 49 | 43, 44, 45, 46, 47, 48 | caovord3 7646 |
. . . 4
⊢ ((((𝐵 +P
𝐶) ∈ P
∧ (𝑤
+P 𝑣) ∈ P) ∧ ((𝑧 +P
𝑢)
+P (𝐵 +P 𝐶)) = ((𝑤 +P 𝑣) +P
(𝐴
+P 𝐷))) → ((𝑧 +P 𝑢)<P
(𝑤
+P 𝑣) ↔ (𝐴 +P 𝐷)<P
(𝐵
+P 𝐶))) |
| 50 | 16, 42, 49 | syl6an 684 |
. . 3
⊢ ((((𝑧 ∈ P ∧
𝑤 ∈ P)
∧ (𝐴 ∈
P ∧ 𝐵
∈ P)) ∧ ((𝑣 ∈ P ∧ 𝑢 ∈ P) ∧
(𝐶 ∈ P
∧ 𝐷 ∈
P))) → (([〈𝑧, 𝑤〉] ~R =
[〈𝐴, 𝐵〉] ~R ∧
[〈𝑣, 𝑢〉]
~R = [〈𝐶, 𝐷〉] ~R ) →
((𝑧
+P 𝑢)<P (𝑤 +P
𝑣) ↔ (𝐴 +P
𝐷)<P (𝐵 +P
𝐶)))) |
| 51 | 9, 1, 4, 10, 50 | brecop 8850 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝐶 ∈
P ∧ 𝐷
∈ P)) → ([〈𝐴, 𝐵〉] ~R
<R [〈𝐶, 𝐷〉] ~R ↔
(𝐴
+P 𝐷)<P (𝐵 +P
𝐶))) |
| 52 | 3, 4, 5, 6, 7, 8, 51 | brecop2 8851 |
1
⊢
([〈𝐴, 𝐵〉]
~R <R [〈𝐶, 𝐷〉] ~R ↔
(𝐴
+P 𝐷)<P (𝐵 +P
𝐶)) |