Proof of Theorem xpord3lem
Step | Hyp | Ref
| Expression |
1 | | otex 5422 |
. . 3
⊢
〈𝑎, 𝑏, 𝑐〉 ∈ V |
2 | | otex 5422 |
. . 3
⊢
〈𝑑, 𝑒, 𝑓〉 ∈ V |
3 | | eleq1 2825 |
. . . 4
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ 〈𝑎, 𝑏, 𝑐〉 ∈ ((𝐴 × 𝐵) × 𝐶))) |
4 | | 2fveq3 6847 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → (1st
‘(1st ‘𝑥)) = (1st ‘(1st
‘〈𝑎, 𝑏, 𝑐〉))) |
5 | | vex 3449 |
. . . . . . . . . 10
⊢ 𝑎 ∈ V |
6 | | vex 3449 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
7 | | vex 3449 |
. . . . . . . . . 10
⊢ 𝑐 ∈ V |
8 | | ot1stg 7935 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) →
(1st ‘(1st ‘〈𝑎, 𝑏, 𝑐〉)) = 𝑎) |
9 | 5, 6, 7, 8 | mp3an 1461 |
. . . . . . . . 9
⊢
(1st ‘(1st ‘〈𝑎, 𝑏, 𝑐〉)) = 𝑎 |
10 | 4, 9 | eqtrdi 2792 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → (1st
‘(1st ‘𝑥)) = 𝑎) |
11 | 10 | breq1d 5115 |
. . . . . . 7
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → ((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ↔ 𝑎𝑅(1st ‘(1st
‘𝑦)))) |
12 | 10 | eqeq1d 2738 |
. . . . . . 7
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → ((1st
‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦)) ↔ 𝑎 = (1st
‘(1st ‘𝑦)))) |
13 | 11, 12 | orbi12d 917 |
. . . . . 6
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → (((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ∨
(1st ‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ↔ (𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))))) |
14 | | 2fveq3 6847 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → (2nd
‘(1st ‘𝑥)) = (2nd ‘(1st
‘〈𝑎, 𝑏, 𝑐〉))) |
15 | | ot2ndg 7936 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) →
(2nd ‘(1st ‘〈𝑎, 𝑏, 𝑐〉)) = 𝑏) |
16 | 5, 6, 7, 15 | mp3an 1461 |
. . . . . . . . 9
⊢
(2nd ‘(1st ‘〈𝑎, 𝑏, 𝑐〉)) = 𝑏 |
17 | 14, 16 | eqtrdi 2792 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → (2nd
‘(1st ‘𝑥)) = 𝑏) |
18 | 17 | breq1d 5115 |
. . . . . . 7
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → ((2nd
‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ↔ 𝑏𝑆(2nd ‘(1st
‘𝑦)))) |
19 | 17 | eqeq1d 2738 |
. . . . . . 7
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → ((2nd
‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦)) ↔ 𝑏 = (2nd
‘(1st ‘𝑦)))) |
20 | 18, 19 | orbi12d 917 |
. . . . . 6
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → (((2nd
‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ↔ (𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))))) |
21 | | fveq2 6842 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → (2nd ‘𝑥) = (2nd
‘〈𝑎, 𝑏, 𝑐〉)) |
22 | | ot3rdg 7937 |
. . . . . . . . . 10
⊢ (𝑐 ∈ V → (2nd
‘〈𝑎, 𝑏, 𝑐〉) = 𝑐) |
23 | 22 | elv 3451 |
. . . . . . . . 9
⊢
(2nd ‘〈𝑎, 𝑏, 𝑐〉) = 𝑐 |
24 | 21, 23 | eqtrdi 2792 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → (2nd ‘𝑥) = 𝑐) |
25 | 24 | breq1d 5115 |
. . . . . . 7
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ↔ 𝑐𝑇(2nd ‘𝑦))) |
26 | 24 | eqeq1d 2738 |
. . . . . . 7
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → ((2nd ‘𝑥) = (2nd ‘𝑦) ↔ 𝑐 = (2nd ‘𝑦))) |
27 | 25, 26 | orbi12d 917 |
. . . . . 6
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → (((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ↔ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦)))) |
28 | 13, 20, 27 | 3anbi123d 1436 |
. . . . 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 ‘𝑦))))) |
29 | | neeq1 3006 |
. . . . 5
⊢ (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → (𝑥 ≠ 𝑦 ↔ 〈𝑎, 𝑏, 𝑐〉 ≠ 𝑦)) |
30 | 28, 29 | anbi12d 631 |
. . . 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 ‘𝑦))) ∧ 〈𝑎, 𝑏, 𝑐〉 ≠ 𝑦))) |
31 | 3, 30 | 3anbi13d 1438 |
. . 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 ‘𝑦))) ∧ 〈𝑎, 𝑏, 𝑐〉 ≠ 𝑦)))) |
32 | | eleq1 2825 |
. . . 4
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ 〈𝑑, 𝑒, 𝑓〉 ∈ ((𝐴 × 𝐵) × 𝐶))) |
33 | | 2fveq3 6847 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (1st
‘(1st ‘𝑦)) = (1st ‘(1st
‘〈𝑑, 𝑒, 𝑓〉))) |
34 | | vex 3449 |
. . . . . . . . . 10
⊢ 𝑑 ∈ V |
35 | | vex 3449 |
. . . . . . . . . 10
⊢ 𝑒 ∈ V |
36 | | vex 3449 |
. . . . . . . . . 10
⊢ 𝑓 ∈ V |
37 | | ot1stg 7935 |
. . . . . . . . . 10
⊢ ((𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V) →
(1st ‘(1st ‘〈𝑑, 𝑒, 𝑓〉)) = 𝑑) |
38 | 34, 35, 36, 37 | mp3an 1461 |
. . . . . . . . 9
⊢
(1st ‘(1st ‘〈𝑑, 𝑒, 𝑓〉)) = 𝑑 |
39 | 33, 38 | eqtrdi 2792 |
. . . . . . . 8
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (1st
‘(1st ‘𝑦)) = 𝑑) |
40 | 39 | breq2d 5117 |
. . . . . . 7
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (𝑎𝑅(1st ‘(1st
‘𝑦)) ↔ 𝑎𝑅𝑑)) |
41 | 39 | eqeq2d 2747 |
. . . . . . 7
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (𝑎 = (1st ‘(1st
‘𝑦)) ↔ 𝑎 = 𝑑)) |
42 | 40, 41 | orbi12d 917 |
. . . . . 6
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → ((𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))) ↔ (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑))) |
43 | | 2fveq3 6847 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (2nd
‘(1st ‘𝑦)) = (2nd ‘(1st
‘〈𝑑, 𝑒, 𝑓〉))) |
44 | | ot2ndg 7936 |
. . . . . . . . . 10
⊢ ((𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V) →
(2nd ‘(1st ‘〈𝑑, 𝑒, 𝑓〉)) = 𝑒) |
45 | 34, 35, 36, 44 | mp3an 1461 |
. . . . . . . . 9
⊢
(2nd ‘(1st ‘〈𝑑, 𝑒, 𝑓〉)) = 𝑒 |
46 | 43, 45 | eqtrdi 2792 |
. . . . . . . 8
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (2nd
‘(1st ‘𝑦)) = 𝑒) |
47 | 46 | breq2d 5117 |
. . . . . . 7
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (𝑏𝑆(2nd ‘(1st
‘𝑦)) ↔ 𝑏𝑆𝑒)) |
48 | 46 | eqeq2d 2747 |
. . . . . . 7
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (𝑏 = (2nd ‘(1st
‘𝑦)) ↔ 𝑏 = 𝑒)) |
49 | 47, 48 | orbi12d 917 |
. . . . . 6
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → ((𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))) ↔ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒))) |
50 | | fveq2 6842 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (2nd ‘𝑦) = (2nd
‘〈𝑑, 𝑒, 𝑓〉)) |
51 | | ot3rdg 7937 |
. . . . . . . . . 10
⊢ (𝑓 ∈ V → (2nd
‘〈𝑑, 𝑒, 𝑓〉) = 𝑓) |
52 | 51 | elv 3451 |
. . . . . . . . 9
⊢
(2nd ‘〈𝑑, 𝑒, 𝑓〉) = 𝑓 |
53 | 50, 52 | eqtrdi 2792 |
. . . . . . . 8
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (2nd ‘𝑦) = 𝑓) |
54 | 53 | breq2d 5117 |
. . . . . . 7
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (𝑐𝑇(2nd ‘𝑦) ↔ 𝑐𝑇𝑓)) |
55 | 53 | eqeq2d 2747 |
. . . . . . 7
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (𝑐 = (2nd ‘𝑦) ↔ 𝑐 = 𝑓)) |
56 | 54, 55 | orbi12d 917 |
. . . . . 6
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → ((𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦)) ↔ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))) |
57 | 42, 49, 56 | 3anbi123d 1436 |
. . . . 5
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (((𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ↔ ((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)))) |
58 | | neeq2 3007 |
. . . . 5
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → (〈𝑎, 𝑏, 𝑐〉 ≠ 𝑦 ↔ 〈𝑎, 𝑏, 𝑐〉 ≠ 〈𝑑, 𝑒, 𝑓〉)) |
59 | 57, 58 | anbi12d 631 |
. . . 4
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → ((((𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ 〈𝑎, 𝑏, 𝑐〉 ≠ 𝑦) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ 〈𝑎, 𝑏, 𝑐〉 ≠ 〈𝑑, 𝑒, 𝑓〉))) |
60 | 32, 59 | 3anbi23d 1439 |
. . 3
⊢ (𝑦 = 〈𝑑, 𝑒, 𝑓〉 → ((〈𝑎, 𝑏, 𝑐〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ 〈𝑎, 𝑏, 𝑐〉 ≠ 𝑦)) ↔ (〈𝑎, 𝑏, 𝑐〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 〈𝑑, 𝑒, 𝑓〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ 〈𝑎, 𝑏, 𝑐〉 ≠ 〈𝑑, 𝑒, 𝑓〉)))) |
61 | | xpord3.1 |
. . 3
⊢ 𝑈 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ∨
(1st ‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ∧
((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ∧
((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} |
62 | 1, 2, 31, 60, 61 | brab 5500 |
. 2
⊢
(〈𝑎, 𝑏, 𝑐〉𝑈〈𝑑, 𝑒, 𝑓〉 ↔ (〈𝑎, 𝑏, 𝑐〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 〈𝑑, 𝑒, 𝑓〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ 〈𝑎, 𝑏, 𝑐〉 ≠ 〈𝑑, 𝑒, 𝑓〉))) |
63 | | otelxp 5676 |
. . 3
⊢
(〈𝑎, 𝑏, 𝑐〉 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) |
64 | | otelxp 5676 |
. . 3
⊢
(〈𝑑, 𝑒, 𝑓〉 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) |
65 | 5, 6, 7 | otthne 5443 |
. . . 4
⊢
(〈𝑎, 𝑏, 𝑐〉 ≠ 〈𝑑, 𝑒, 𝑓〉 ↔ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) |
66 | 65 | anbi2i 623 |
. . 3
⊢ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ 〈𝑎, 𝑏, 𝑐〉 ≠ 〈𝑑, 𝑒, 𝑓〉) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))) |
67 | 63, 64, 66 | 3anbi123i 1155 |
. 2
⊢
((〈𝑎, 𝑏, 𝑐〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 〈𝑑, 𝑒, 𝑓〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ 〈𝑎, 𝑏, 𝑐〉 ≠ 〈𝑑, 𝑒, 𝑓〉)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))) |
68 | 62, 67 | bitri 274 |
1
⊢
(〈𝑎, 𝑏, 𝑐〉𝑈〈𝑑, 𝑒, 𝑓〉 ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))) |