Proof of Theorem xpord3lem
Step | Hyp | Ref
| Expression |
1 | | opex 5319 |
. . 3
⊢
〈〈𝑎, 𝑏〉, 𝑐〉 ∈ V |
2 | | opex 5319 |
. . 3
⊢
〈〈𝑑, 𝑒〉, 𝑓〉 ∈ V |
3 | | eleq1 2820 |
. . . 4
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ 〈〈𝑎, 𝑏〉, 𝑐〉 ∈ ((𝐴 × 𝐵) × 𝐶))) |
4 | | vex 3401 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
5 | | vex 3401 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
6 | | vex 3401 |
. . . . . . . . 9
⊢ 𝑐 ∈ V |
7 | 4, 5, 6 | ot21std 33246 |
. . . . . . . 8
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → (1st
‘(1st ‘𝑥)) = 𝑎) |
8 | 7 | breq1d 5037 |
. . . . . . 7
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → ((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ↔ 𝑎𝑅(1st ‘(1st
‘𝑦)))) |
9 | 7 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → ((1st
‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦)) ↔ 𝑎 = (1st
‘(1st ‘𝑦)))) |
10 | 8, 9 | orbi12d 918 |
. . . . . 6
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → (((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ∨
(1st ‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ↔ (𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))))) |
11 | 4, 5, 6 | ot22ndd 33247 |
. . . . . . . 8
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → (2nd
‘(1st ‘𝑥)) = 𝑏) |
12 | 11 | breq1d 5037 |
. . . . . . 7
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → ((2nd
‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ↔ 𝑏𝑆(2nd ‘(1st
‘𝑦)))) |
13 | 11 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → ((2nd
‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦)) ↔ 𝑏 = (2nd
‘(1st ‘𝑦)))) |
14 | 12, 13 | orbi12d 918 |
. . . . . 6
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → (((2nd
‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ↔ (𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))))) |
15 | | opex 5319 |
. . . . . . . . 9
⊢
〈𝑎, 𝑏〉 ∈ V |
16 | 15, 6 | op2ndd 7718 |
. . . . . . . 8
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → (2nd ‘𝑥) = 𝑐) |
17 | 16 | breq1d 5037 |
. . . . . . 7
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ↔ 𝑐𝑇(2nd ‘𝑦))) |
18 | 16 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → ((2nd ‘𝑥) = (2nd ‘𝑦) ↔ 𝑐 = (2nd ‘𝑦))) |
19 | 17, 18 | orbi12d 918 |
. . . . . 6
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → (((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ↔ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦)))) |
20 | 10, 14, 19 | 3anbi123d 1437 |
. . . . 5
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → ((((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ∨
(1st ‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ∧
((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ∧
((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ↔ ((𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))))) |
21 | | neeq1 2996 |
. . . . 5
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → (𝑥 ≠ 𝑦 ↔ 〈〈𝑎, 𝑏〉, 𝑐〉 ≠ 𝑦)) |
22 | 20, 21 | anbi12d 634 |
. . . 4
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → (((((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ∨
(1st ‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ∧
((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ∧
((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦) ↔ (((𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ 〈〈𝑎, 𝑏〉, 𝑐〉 ≠ 𝑦))) |
23 | 3, 22 | 3anbi13d 1439 |
. . 3
⊢ (𝑥 = 〈〈𝑎, 𝑏〉, 𝑐〉 → ((𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ∨
(1st ‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ∧
((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ∧
((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦)) ↔ (〈〈𝑎, 𝑏〉, 𝑐〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ 〈〈𝑎, 𝑏〉, 𝑐〉 ≠ 𝑦)))) |
24 | | eleq1 2820 |
. . . 4
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ 〈〈𝑑, 𝑒〉, 𝑓〉 ∈ ((𝐴 × 𝐵) × 𝐶))) |
25 | | vex 3401 |
. . . . . . . . 9
⊢ 𝑑 ∈ V |
26 | | vex 3401 |
. . . . . . . . 9
⊢ 𝑒 ∈ V |
27 | | vex 3401 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
28 | 25, 26, 27 | ot21std 33246 |
. . . . . . . 8
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (1st
‘(1st ‘𝑦)) = 𝑑) |
29 | 28 | breq2d 5039 |
. . . . . . 7
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑎𝑅(1st ‘(1st
‘𝑦)) ↔ 𝑎𝑅𝑑)) |
30 | 28 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑎 = (1st ‘(1st
‘𝑦)) ↔ 𝑎 = 𝑑)) |
31 | 29, 30 | orbi12d 918 |
. . . . . 6
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → ((𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))) ↔ (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑))) |
32 | 25, 26, 27 | ot22ndd 33247 |
. . . . . . . 8
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (2nd
‘(1st ‘𝑦)) = 𝑒) |
33 | 32 | breq2d 5039 |
. . . . . . 7
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑏𝑆(2nd ‘(1st
‘𝑦)) ↔ 𝑏𝑆𝑒)) |
34 | 32 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑏 = (2nd ‘(1st
‘𝑦)) ↔ 𝑏 = 𝑒)) |
35 | 33, 34 | orbi12d 918 |
. . . . . 6
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → ((𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))) ↔ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒))) |
36 | | opex 5319 |
. . . . . . . . 9
⊢
〈𝑑, 𝑒〉 ∈ V |
37 | 36, 27 | op2ndd 7718 |
. . . . . . . 8
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (2nd ‘𝑦) = 𝑓) |
38 | 37 | breq2d 5039 |
. . . . . . 7
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑐𝑇(2nd ‘𝑦) ↔ 𝑐𝑇𝑓)) |
39 | 37 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑐 = (2nd ‘𝑦) ↔ 𝑐 = 𝑓)) |
40 | 38, 39 | orbi12d 918 |
. . . . . 6
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → ((𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦)) ↔ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))) |
41 | 31, 35, 40 | 3anbi123d 1437 |
. . . . 5
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (((𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ↔ ((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)))) |
42 | | neeq2 2997 |
. . . . 5
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (〈〈𝑎, 𝑏〉, 𝑐〉 ≠ 𝑦 ↔ 〈〈𝑎, 𝑏〉, 𝑐〉 ≠ 〈〈𝑑, 𝑒〉, 𝑓〉)) |
43 | 41, 42 | anbi12d 634 |
. . . 4
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → ((((𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ 〈〈𝑎, 𝑏〉, 𝑐〉 ≠ 𝑦) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ 〈〈𝑎, 𝑏〉, 𝑐〉 ≠ 〈〈𝑑, 𝑒〉, 𝑓〉))) |
44 | 24, 43 | 3anbi23d 1440 |
. . 3
⊢ (𝑦 = 〈〈𝑑, 𝑒〉, 𝑓〉 → ((〈〈𝑎, 𝑏〉, 𝑐〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ 〈〈𝑎, 𝑏〉, 𝑐〉 ≠ 𝑦)) ↔ (〈〈𝑎, 𝑏〉, 𝑐〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 〈〈𝑑, 𝑒〉, 𝑓〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ 〈〈𝑎, 𝑏〉, 𝑐〉 ≠ 〈〈𝑑, 𝑒〉, 𝑓〉)))) |
45 | | xpord3.1 |
. . 3
⊢ 𝑈 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ∨
(1st ‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ∧
((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ∧
((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} |
46 | 1, 2, 23, 44, 45 | brab 5395 |
. 2
⊢
(〈〈𝑎,
𝑏〉, 𝑐〉𝑈〈〈𝑑, 𝑒〉, 𝑓〉 ↔ (〈〈𝑎, 𝑏〉, 𝑐〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 〈〈𝑑, 𝑒〉, 𝑓〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ 〈〈𝑎, 𝑏〉, 𝑐〉 ≠ 〈〈𝑑, 𝑒〉, 𝑓〉))) |
47 | | ot2elxp 33245 |
. . 3
⊢
(〈〈𝑎,
𝑏〉, 𝑐〉 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) |
48 | | ot2elxp 33245 |
. . 3
⊢
(〈〈𝑑,
𝑒〉, 𝑓〉 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) |
49 | 4, 5, 6 | otthne 33248 |
. . . 4
⊢
(〈〈𝑎,
𝑏〉, 𝑐〉 ≠ 〈〈𝑑, 𝑒〉, 𝑓〉 ↔ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) |
50 | 49 | anbi2i 626 |
. . 3
⊢ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ 〈〈𝑎, 𝑏〉, 𝑐〉 ≠ 〈〈𝑑, 𝑒〉, 𝑓〉) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))) |
51 | 47, 48, 50 | 3anbi123i 1156 |
. 2
⊢
((〈〈𝑎,
𝑏〉, 𝑐〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 〈〈𝑑, 𝑒〉, 𝑓〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ 〈〈𝑎, 𝑏〉, 𝑐〉 ≠ 〈〈𝑑, 𝑒〉, 𝑓〉)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))) |
52 | 46, 51 | bitri 278 |
1
⊢
(〈〈𝑎,
𝑏〉, 𝑐〉𝑈〈〈𝑑, 𝑒〉, 𝑓〉 ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))) |