| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | enrer 11104 | . . . . . . . . . . . . . . . 16
⊢ 
~R Er (P ×
P) | 
| 2 | 1 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
~R Er (P ×
P)) | 
| 3 |  | prsrlem1 11113 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
((((𝑤 ∈
P ∧ 𝑣
∈ P) ∧ (𝑠 ∈ P ∧ 𝑓 ∈ P)) ∧
((𝑢 ∈ P
∧ 𝑡 ∈
P) ∧ (𝑔
∈ P ∧ ℎ ∈ P))) ∧ ((𝑤 +P
𝑓) = (𝑣 +P 𝑠) ∧ (𝑢 +P ℎ) = (𝑡 +P 𝑔)))) | 
| 4 |  | addcmpblnr 11110 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑤 ∈ P ∧
𝑣 ∈ P)
∧ (𝑠 ∈
P ∧ 𝑓
∈ P)) ∧ ((𝑢 ∈ P ∧ 𝑡 ∈ P) ∧
(𝑔 ∈ P
∧ ℎ ∈
P))) → (((𝑤 +P 𝑓) = (𝑣 +P 𝑠) ∧ (𝑢 +P ℎ) = (𝑡 +P 𝑔)) → 〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉
~R 〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉)) | 
| 5 | 4 | imp 406 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑤 ∈
P ∧ 𝑣
∈ P) ∧ (𝑠 ∈ P ∧ 𝑓 ∈ P)) ∧
((𝑢 ∈ P
∧ 𝑡 ∈
P) ∧ (𝑔
∈ P ∧ ℎ ∈ P))) ∧ ((𝑤 +P
𝑓) = (𝑣 +P 𝑠) ∧ (𝑢 +P ℎ) = (𝑡 +P 𝑔))) → 〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉
~R 〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉) | 
| 6 | 3, 5 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
〈(𝑤
+P 𝑢), (𝑣 +P 𝑡)〉
~R 〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉) | 
| 7 | 2, 6 | erthi 8799 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
[〈(𝑤
+P 𝑢), (𝑣 +P 𝑡)〉]
~R = [〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉]
~R ) | 
| 8 | 7 | adantrlr 723 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ (𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
[〈(𝑤
+P 𝑢), (𝑣 +P 𝑡)〉]
~R = [〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉]
~R ) | 
| 9 | 8 | adantrrr 725 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ))) → [〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉]
~R = [〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉]
~R ) | 
| 10 |  | simprlr 779 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ))) → 𝑧 = [〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉]
~R ) | 
| 11 |  | simprrr 781 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ))) → 𝑞 = [〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉]
~R ) | 
| 12 | 9, 10, 11 | 3eqtr4d 2786 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ))) → 𝑧 = 𝑞) | 
| 13 | 12 | expr 456 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) → (((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ) → 𝑧 = 𝑞)) | 
| 14 | 13 | exlimdvv 1933 | . . . . . . . . 9
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) → (∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ) → 𝑧 = 𝑞)) | 
| 15 | 14 | exlimdvv 1933 | . . . . . . . 8
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) → (∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ) → 𝑧 = 𝑞)) | 
| 16 | 15 | ex 412 | . . . . . . 7
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
(((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) → (∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ) → 𝑧 = 𝑞))) | 
| 17 | 16 | exlimdvv 1933 | . . . . . 6
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
(∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) → (∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ) → 𝑧 = 𝑞))) | 
| 18 | 17 | exlimdvv 1933 | . . . . 5
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
(∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) → (∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ) → 𝑧 = 𝑞))) | 
| 19 | 18 | impd 410 | . . . 4
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R )) → 𝑧 = 𝑞)) | 
| 20 | 19 | alrimivv 1927 | . . 3
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R )) → 𝑧 = 𝑞)) | 
| 21 |  | opeq12 4874 | . . . . . . . . . . 11
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 〈𝑤, 𝑣〉 = 〈𝑠, 𝑓〉) | 
| 22 | 21 | eceq1d 8786 | . . . . . . . . . 10
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → [〈𝑤, 𝑣〉] ~R =
[〈𝑠, 𝑓〉]
~R ) | 
| 23 | 22 | eqeq2d 2747 | . . . . . . . . 9
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝐴 = [〈𝑤, 𝑣〉] ~R ↔
𝐴 = [〈𝑠, 𝑓〉] ~R
)) | 
| 24 | 23 | anbi1d 631 | . . . . . . . 8
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ↔
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R
))) | 
| 25 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 𝑤 = 𝑠) | 
| 26 | 25 | oveq1d 7447 | . . . . . . . . . . 11
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝑤 +P 𝑢) = (𝑠 +P 𝑢)) | 
| 27 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 𝑣 = 𝑓) | 
| 28 | 27 | oveq1d 7447 | . . . . . . . . . . 11
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝑣 +P 𝑡) = (𝑓 +P 𝑡)) | 
| 29 | 26, 28 | opeq12d 4880 | . . . . . . . . . 10
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉 = 〈(𝑠 +P
𝑢), (𝑓 +P 𝑡)〉) | 
| 30 | 29 | eceq1d 8786 | . . . . . . . . 9
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → [〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉]
~R = [〈(𝑠 +P 𝑢), (𝑓 +P 𝑡)〉]
~R ) | 
| 31 | 30 | eqeq2d 2747 | . . . . . . . 8
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝑞 = [〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉]
~R ↔ 𝑞 = [〈(𝑠 +P 𝑢), (𝑓 +P 𝑡)〉]
~R )) | 
| 32 | 24, 31 | anbi12d 632 | . . . . . . 7
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ↔ ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑢), (𝑓 +P 𝑡)〉]
~R ))) | 
| 33 |  | opeq12 4874 | . . . . . . . . . . 11
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 〈𝑢, 𝑡〉 = 〈𝑔, ℎ〉) | 
| 34 | 33 | eceq1d 8786 | . . . . . . . . . 10
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → [〈𝑢, 𝑡〉] ~R =
[〈𝑔, ℎ〉]
~R ) | 
| 35 | 34 | eqeq2d 2747 | . . . . . . . . 9
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝐵 = [〈𝑢, 𝑡〉] ~R ↔
𝐵 = [〈𝑔, ℎ〉] ~R
)) | 
| 36 | 35 | anbi2d 630 | . . . . . . . 8
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ↔
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R
))) | 
| 37 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 𝑢 = 𝑔) | 
| 38 | 37 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝑠 +P 𝑢) = (𝑠 +P 𝑔)) | 
| 39 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 𝑡 = ℎ) | 
| 40 | 39 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝑓 +P 𝑡) = (𝑓 +P ℎ)) | 
| 41 | 38, 40 | opeq12d 4880 | . . . . . . . . . 10
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 〈(𝑠 +P 𝑢), (𝑓 +P 𝑡)〉 = 〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉) | 
| 42 | 41 | eceq1d 8786 | . . . . . . . . 9
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → [〈(𝑠 +P 𝑢), (𝑓 +P 𝑡)〉]
~R = [〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉]
~R ) | 
| 43 | 42 | eqeq2d 2747 | . . . . . . . 8
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝑞 = [〈(𝑠 +P 𝑢), (𝑓 +P 𝑡)〉]
~R ↔ 𝑞 = [〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉]
~R )) | 
| 44 | 36, 43 | anbi12d 632 | . . . . . . 7
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑢), (𝑓 +P 𝑡)〉]
~R ) ↔ ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ))) | 
| 45 | 32, 44 | cbvex4vw 2040 | . . . . . 6
⊢
(∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ↔ ∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R )) | 
| 46 | 45 | anbi2i 623 | . . . . 5
⊢
((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) ↔ (∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ))) | 
| 47 | 46 | imbi1i 349 | . . . 4
⊢
(((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) → 𝑧 = 𝑞) ↔ ((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R )) → 𝑧 = 𝑞)) | 
| 48 | 47 | 2albii 1819 | . . 3
⊢
(∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) → 𝑧 = 𝑞) ↔ ∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R )) → 𝑧 = 𝑞)) | 
| 49 | 20, 48 | sylibr 234 | . 2
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) → 𝑧 = 𝑞)) | 
| 50 |  | eqeq1 2740 | . . . . 5
⊢ (𝑧 = 𝑞 → (𝑧 = [〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉]
~R ↔ 𝑞 = [〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉]
~R )) | 
| 51 | 50 | anbi2d 630 | . . . 4
⊢ (𝑧 = 𝑞 → (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ↔ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ))) | 
| 52 | 51 | 4exbidv 1925 | . . 3
⊢ (𝑧 = 𝑞 → (∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ↔ ∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ))) | 
| 53 | 52 | mo4 2565 | . 2
⊢
(∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ↔ ∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) → 𝑧 = 𝑞)) | 
| 54 | 49, 53 | sylibr 234 | 1
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) |