Proof of Theorem xpord2lem
Step | Hyp | Ref
| Expression |
1 | | opex 5332 |
. 2
⊢
〈𝑎, 𝑏〉 ∈ V |
2 | | opex 5332 |
. 2
⊢
〈𝑐, 𝑑〉 ∈ V |
3 | | eleq1 2821 |
. . . 4
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (𝑥 ∈ (𝐴 × 𝐵) ↔ 〈𝑎, 𝑏〉 ∈ (𝐴 × 𝐵))) |
4 | | opelxp 5571 |
. . . 4
⊢
(〈𝑎, 𝑏〉 ∈ (𝐴 × 𝐵) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) |
5 | 3, 4 | bitrdi 290 |
. . 3
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (𝑥 ∈ (𝐴 × 𝐵) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵))) |
6 | | vex 3404 |
. . . . . . 7
⊢ 𝑎 ∈ V |
7 | | vex 3404 |
. . . . . . 7
⊢ 𝑏 ∈ V |
8 | 6, 7 | op1std 7736 |
. . . . . 6
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (1st ‘𝑥) = 𝑎) |
9 | 8 | breq1d 5050 |
. . . . 5
⊢ (𝑥 = 〈𝑎, 𝑏〉 → ((1st ‘𝑥)𝑅(1st ‘𝑦) ↔ 𝑎𝑅(1st ‘𝑦))) |
10 | 8 | eqeq1d 2741 |
. . . . 5
⊢ (𝑥 = 〈𝑎, 𝑏〉 → ((1st ‘𝑥) = (1st ‘𝑦) ↔ 𝑎 = (1st ‘𝑦))) |
11 | 9, 10 | orbi12d 918 |
. . . 4
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ↔ (𝑎𝑅(1st ‘𝑦) ∨ 𝑎 = (1st ‘𝑦)))) |
12 | 6, 7 | op2ndd 7737 |
. . . . . 6
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (2nd ‘𝑥) = 𝑏) |
13 | 12 | breq1d 5050 |
. . . . 5
⊢ (𝑥 = 〈𝑎, 𝑏〉 → ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ↔ 𝑏𝑆(2nd ‘𝑦))) |
14 | 12 | eqeq1d 2741 |
. . . . 5
⊢ (𝑥 = 〈𝑎, 𝑏〉 → ((2nd ‘𝑥) = (2nd ‘𝑦) ↔ 𝑏 = (2nd ‘𝑦))) |
15 | 13, 14 | orbi12d 918 |
. . . 4
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (((2nd ‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ↔ (𝑏𝑆(2nd ‘𝑦) ∨ 𝑏 = (2nd ‘𝑦)))) |
16 | | neeq1 2997 |
. . . 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 2821 |
. . . 4
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (𝑦 ∈ (𝐴 × 𝐵) ↔ 〈𝑐, 𝑑〉 ∈ (𝐴 × 𝐵))) |
20 | | opelxp 5571 |
. . . 4
⊢
(〈𝑐, 𝑑〉 ∈ (𝐴 × 𝐵) ↔ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) |
21 | 19, 20 | bitrdi 290 |
. . 3
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (𝑦 ∈ (𝐴 × 𝐵) ↔ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) |
22 | | vex 3404 |
. . . . . . 7
⊢ 𝑐 ∈ V |
23 | | vex 3404 |
. . . . . . 7
⊢ 𝑑 ∈ V |
24 | 22, 23 | op1std 7736 |
. . . . . 6
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (1st ‘𝑦) = 𝑐) |
25 | 24 | breq2d 5052 |
. . . . 5
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (𝑎𝑅(1st ‘𝑦) ↔ 𝑎𝑅𝑐)) |
26 | 24 | eqeq2d 2750 |
. . . . 5
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (𝑎 = (1st ‘𝑦) ↔ 𝑎 = 𝑐)) |
27 | 25, 26 | orbi12d 918 |
. . . 4
⊢ (𝑦 = 〈𝑐, 𝑑〉 → ((𝑎𝑅(1st ‘𝑦) ∨ 𝑎 = (1st ‘𝑦)) ↔ (𝑎𝑅𝑐 ∨ 𝑎 = 𝑐))) |
28 | 22, 23 | op2ndd 7737 |
. . . . . 6
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (2nd ‘𝑦) = 𝑑) |
29 | 28 | breq2d 5052 |
. . . . 5
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (𝑏𝑆(2nd ‘𝑦) ↔ 𝑏𝑆𝑑)) |
30 | 28 | eqeq2d 2750 |
. . . . 5
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (𝑏 = (2nd ‘𝑦) ↔ 𝑏 = 𝑑)) |
31 | 29, 30 | orbi12d 918 |
. . . 4
⊢ (𝑦 = 〈𝑐, 𝑑〉 → ((𝑏𝑆(2nd ‘𝑦) ∨ 𝑏 = (2nd ‘𝑦)) ↔ (𝑏𝑆𝑑 ∨ 𝑏 = 𝑑))) |
32 | | neeq2 2998 |
. . . . 5
⊢ (𝑦 = 〈𝑐, 𝑑〉 → (〈𝑎, 𝑏〉 ≠ 𝑦 ↔ 〈𝑎, 𝑏〉 ≠ 〈𝑐, 𝑑〉)) |
33 | 6, 7 | opthne 5350 |
. . . . 5
⊢
(〈𝑎, 𝑏〉 ≠ 〈𝑐, 𝑑〉 ↔ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑)) |
34 | 32, 33 | bitrdi 290 |
. . . 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 5408 |
1
⊢
(〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐) ∧ (𝑏𝑆𝑑 ∨ 𝑏 = 𝑑) ∧ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑)))) |