Proof of Theorem xpord2lem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | opex 5468 | . 2
⊢
〈𝑎, 𝑏〉 ∈ V | 
| 2 |  | opex 5468 | . 2
⊢
〈𝑐, 𝑑〉 ∈ V | 
| 3 |  | eleq1 2828 | . . . 4
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (𝑥 ∈ (𝐴 × 𝐵) ↔ 〈𝑎, 𝑏〉 ∈ (𝐴 × 𝐵))) | 
| 4 |  | opelxp 5720 | . . . 4
⊢
(〈𝑎, 𝑏〉 ∈ (𝐴 × 𝐵) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) | 
| 5 | 3, 4 | bitrdi 287 | . . 3
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (𝑥 ∈ (𝐴 × 𝐵) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵))) | 
| 6 |  | vex 3483 | . . . . . . 7
⊢ 𝑎 ∈ V | 
| 7 |  | vex 3483 | . . . . . . 7
⊢ 𝑏 ∈ V | 
| 8 | 6, 7 | op1std 8025 | . . . . . 6
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (1st ‘𝑥) = 𝑎) | 
| 9 | 8 | breq1d 5152 | . . . . 5
⊢ (𝑥 = 〈𝑎, 𝑏〉 → ((1st ‘𝑥)𝑅(1st ‘𝑦) ↔ 𝑎𝑅(1st ‘𝑦))) | 
| 10 | 8 | eqeq1d 2738 | . . . . 5
⊢ (𝑥 = 〈𝑎, 𝑏〉 → ((1st ‘𝑥) = (1st ‘𝑦) ↔ 𝑎 = (1st ‘𝑦))) | 
| 11 | 9, 10 | orbi12d 918 | . . . 4
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ↔ (𝑎𝑅(1st ‘𝑦) ∨ 𝑎 = (1st ‘𝑦)))) | 
| 12 | 6, 7 | op2ndd 8026 | . . . . . 6
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (2nd ‘𝑥) = 𝑏) | 
| 13 | 12 | breq1d 5152 | . . . . 5
⊢ (𝑥 = 〈𝑎, 𝑏〉 → ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ↔ 𝑏𝑆(2nd ‘𝑦))) | 
| 14 | 12 | eqeq1d 2738 | . . . . 5
⊢ (𝑥 = 〈𝑎, 𝑏〉 → ((2nd ‘𝑥) = (2nd ‘𝑦) ↔ 𝑏 = (2nd ‘𝑦))) | 
| 15 | 13, 14 | orbi12d 918 | . . . 4
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (((2nd ‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ↔ (𝑏𝑆(2nd ‘𝑦) ∨ 𝑏 = (2nd ‘𝑦)))) | 
| 16 |  | neeq1 3002 | . . . 4
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (𝑥 ≠ 𝑦 ↔ 〈𝑎, 𝑏〉 ≠ 𝑦)) | 
| 17 | 11, 15, 16 | 3anbi123d 1437 | . . 3
⊢ (𝑥 = 〈𝑎, 𝑏〉 → ((((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦) ↔ ((𝑎𝑅(1st ‘𝑦) ∨ 𝑎 = (1st ‘𝑦)) ∧ (𝑏𝑆(2nd ‘𝑦) ∨ 𝑏 = (2nd ‘𝑦)) ∧ 〈𝑎, 𝑏〉 ≠ 𝑦))) | 
| 18 | 5, 17 | 3anbi13d 1439 | . 2
⊢ (𝑥 = 〈𝑎, 𝑏〉 → ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ ((𝑎𝑅(1st ‘𝑦) ∨ 𝑎 = (1st ‘𝑦)) ∧ (𝑏𝑆(2nd ‘𝑦) ∨ 𝑏 = (2nd ‘𝑦)) ∧ 〈𝑎, 𝑏〉 ≠ 𝑦)))) | 
| 19 |  | eleq1 2828 | . . . 4
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (𝑦 ∈ (𝐴 × 𝐵) ↔ 〈𝑐, 𝑑〉 ∈ (𝐴 × 𝐵))) | 
| 20 |  | opelxp 5720 | . . . 4
⊢
(〈𝑐, 𝑑〉 ∈ (𝐴 × 𝐵) ↔ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) | 
| 21 | 19, 20 | bitrdi 287 | . . 3
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (𝑦 ∈ (𝐴 × 𝐵) ↔ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) | 
| 22 |  | vex 3483 | . . . . . . 7
⊢ 𝑐 ∈ V | 
| 23 |  | vex 3483 | . . . . . . 7
⊢ 𝑑 ∈ V | 
| 24 | 22, 23 | op1std 8025 | . . . . . 6
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (1st ‘𝑦) = 𝑐) | 
| 25 | 24 | breq2d 5154 | . . . . 5
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (𝑎𝑅(1st ‘𝑦) ↔ 𝑎𝑅𝑐)) | 
| 26 | 24 | eqeq2d 2747 | . . . . 5
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (𝑎 = (1st ‘𝑦) ↔ 𝑎 = 𝑐)) | 
| 27 | 25, 26 | orbi12d 918 | . . . 4
⊢ (𝑦 = 〈𝑐, 𝑑〉 → ((𝑎𝑅(1st ‘𝑦) ∨ 𝑎 = (1st ‘𝑦)) ↔ (𝑎𝑅𝑐 ∨ 𝑎 = 𝑐))) | 
| 28 | 22, 23 | op2ndd 8026 | . . . . . 6
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (2nd ‘𝑦) = 𝑑) | 
| 29 | 28 | breq2d 5154 | . . . . 5
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (𝑏𝑆(2nd ‘𝑦) ↔ 𝑏𝑆𝑑)) | 
| 30 | 28 | eqeq2d 2747 | . . . . 5
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (𝑏 = (2nd ‘𝑦) ↔ 𝑏 = 𝑑)) | 
| 31 | 29, 30 | orbi12d 918 | . . . 4
⊢ (𝑦 = 〈𝑐, 𝑑〉 → ((𝑏𝑆(2nd ‘𝑦) ∨ 𝑏 = (2nd ‘𝑦)) ↔ (𝑏𝑆𝑑 ∨ 𝑏 = 𝑑))) | 
| 32 |  | neeq2 3003 | . . . . 5
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (〈𝑎, 𝑏〉 ≠ 𝑦 ↔ 〈𝑎, 𝑏〉 ≠ 〈𝑐, 𝑑〉)) | 
| 33 | 6, 7 | opthne 5486 | . . . . 5
⊢
(〈𝑎, 𝑏〉 ≠ 〈𝑐, 𝑑〉 ↔ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑)) | 
| 34 | 32, 33 | bitrdi 287 | . . . 4
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (〈𝑎, 𝑏〉 ≠ 𝑦 ↔ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))) | 
| 35 | 27, 31, 34 | 3anbi123d 1437 | . . 3
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (((𝑎𝑅(1st ‘𝑦) ∨ 𝑎 = (1st ‘𝑦)) ∧ (𝑏𝑆(2nd ‘𝑦) ∨ 𝑏 = (2nd ‘𝑦)) ∧ 〈𝑎, 𝑏〉 ≠ 𝑦) ↔ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐) ∧ (𝑏𝑆𝑑 ∨ 𝑏 = 𝑑) ∧ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑)))) | 
| 36 | 21, 35 | 3anbi23d 1440 | . 2
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ ((𝑎𝑅(1st ‘𝑦) ∨ 𝑎 = (1st ‘𝑦)) ∧ (𝑏𝑆(2nd ‘𝑦) ∨ 𝑏 = (2nd ‘𝑦)) ∧ 〈𝑎, 𝑏〉 ≠ 𝑦)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐) ∧ (𝑏𝑆𝑑 ∨ 𝑏 = 𝑑) ∧ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))))) | 
| 37 |  | xpord2.1 | . 2
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))} | 
| 38 | 1, 2, 18, 36, 37 | brab 5547 | 1
⊢
(〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐) ∧ (𝑏𝑆𝑑 ∨ 𝑏 = 𝑑) ∧ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑)))) |