Step | Hyp | Ref
| Expression |
1 | | otex 5427 |
. . 3
⊢
⟨𝑎, 𝑏, 𝑐⟩ ∈ V |
2 | | otex 5427 |
. . 3
⊢
⟨𝑑, 𝑒, 𝑓⟩ ∈ V |
3 | | eleq1 2826 |
. . . 4
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶))) |
4 | | 2fveq3 6852 |
. . . . . . . . 9
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (1st
‘(1st ‘𝑥)) = (1st ‘(1st
‘⟨𝑎, 𝑏, 𝑐⟩))) |
5 | | vex 3452 |
. . . . . . . . . 10
⊢ 𝑎 ∈ V |
6 | | vex 3452 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
7 | | vex 3452 |
. . . . . . . . . 10
⊢ 𝑐 ∈ V |
8 | | ot1stg 7940 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) →
(1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑎) |
9 | 5, 6, 7, 8 | mp3an 1462 |
. . . . . . . . 9
⊢
(1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑎 |
10 | 4, 9 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (1st
‘(1st ‘𝑥)) = 𝑎) |
11 | 10 | breq1d 5120 |
. . . . . . 7
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ↔ 𝑎𝑅(1st ‘(1st
‘𝑦)))) |
12 | 10 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((1st
‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦)) ↔ 𝑎 = (1st
‘(1st ‘𝑦)))) |
13 | 11, 12 | orbi12d 918 |
. . . . . 6
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ∨
(1st ‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ↔ (𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))))) |
14 | | 2fveq3 6852 |
. . . . . . . . 9
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd
‘(1st ‘𝑥)) = (2nd ‘(1st
‘⟨𝑎, 𝑏, 𝑐⟩))) |
15 | | ot2ndg 7941 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) →
(2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑏) |
16 | 5, 6, 7, 15 | mp3an 1462 |
. . . . . . . . 9
⊢
(2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑏 |
17 | 14, 16 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd
‘(1st ‘𝑥)) = 𝑏) |
18 | 17 | breq1d 5120 |
. . . . . . 7
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd
‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ↔ 𝑏𝑆(2nd ‘(1st
‘𝑦)))) |
19 | 17 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd
‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦)) ↔ 𝑏 = (2nd
‘(1st ‘𝑦)))) |
20 | 18, 19 | orbi12d 918 |
. . . . . 6
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((2nd
‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ↔ (𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))))) |
21 | | fveq2 6847 |
. . . . . . . . 9
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘𝑥) = (2nd
‘⟨𝑎, 𝑏, 𝑐⟩)) |
22 | | ot3rdg 7942 |
. . . . . . . . . 10
⊢ (𝑐 ∈ V → (2nd
‘⟨𝑎, 𝑏, 𝑐⟩) = 𝑐) |
23 | 22 | elv 3454 |
. . . . . . . . 9
⊢
(2nd ‘⟨𝑎, 𝑏, 𝑐⟩) = 𝑐 |
24 | 21, 23 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘𝑥) = 𝑐) |
25 | 24 | breq1d 5120 |
. . . . . . 7
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ↔ 𝑐𝑇(2nd ‘𝑦))) |
26 | 24 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘𝑥) = (2nd ‘𝑦) ↔ 𝑐 = (2nd ‘𝑦))) |
27 | 25, 26 | orbi12d 918 |
. . . . . 6
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ↔ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦)))) |
28 | 13, 20, 27 | 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 ‘𝑦))))) |
29 | | neeq1 3007 |
. . . . 5
⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑥 ≠ 𝑦 ↔ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦)) |
30 | 28, 29 | anbi12d 632 |
. . . 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 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 ‘𝑦))) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦)))) |
32 | | eleq1 2826 |
. . . 4
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶))) |
33 | | 2fveq3 6852 |
. . . . . . . . 9
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (1st
‘(1st ‘𝑦)) = (1st ‘(1st
‘⟨𝑑, 𝑒, 𝑓⟩))) |
34 | | vex 3452 |
. . . . . . . . . 10
⊢ 𝑑 ∈ V |
35 | | vex 3452 |
. . . . . . . . . 10
⊢ 𝑒 ∈ V |
36 | | vex 3452 |
. . . . . . . . . 10
⊢ 𝑓 ∈ V |
37 | | ot1stg 7940 |
. . . . . . . . . 10
⊢ ((𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V) →
(1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑑) |
38 | 34, 35, 36, 37 | mp3an 1462 |
. . . . . . . . 9
⊢
(1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑑 |
39 | 33, 38 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (1st
‘(1st ‘𝑦)) = 𝑑) |
40 | 39 | breq2d 5122 |
. . . . . . 7
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑎𝑅(1st ‘(1st
‘𝑦)) ↔ 𝑎𝑅𝑑)) |
41 | 39 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑎 = (1st ‘(1st
‘𝑦)) ↔ 𝑎 = 𝑑)) |
42 | 40, 41 | orbi12d 918 |
. . . . . 6
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))) ↔ (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑))) |
43 | | 2fveq3 6852 |
. . . . . . . . 9
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd
‘(1st ‘𝑦)) = (2nd ‘(1st
‘⟨𝑑, 𝑒, 𝑓⟩))) |
44 | | ot2ndg 7941 |
. . . . . . . . . 10
⊢ ((𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V) →
(2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑒) |
45 | 34, 35, 36, 44 | mp3an 1462 |
. . . . . . . . 9
⊢
(2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑒 |
46 | 43, 45 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd
‘(1st ‘𝑦)) = 𝑒) |
47 | 46 | breq2d 5122 |
. . . . . . 7
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑏𝑆(2nd ‘(1st
‘𝑦)) ↔ 𝑏𝑆𝑒)) |
48 | 46 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑏 = (2nd ‘(1st
‘𝑦)) ↔ 𝑏 = 𝑒)) |
49 | 47, 48 | orbi12d 918 |
. . . . . 6
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))) ↔ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒))) |
50 | | fveq2 6847 |
. . . . . . . . 9
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘𝑦) = (2nd
‘⟨𝑑, 𝑒, 𝑓⟩)) |
51 | | ot3rdg 7942 |
. . . . . . . . . 10
⊢ (𝑓 ∈ V → (2nd
‘⟨𝑑, 𝑒, 𝑓⟩) = 𝑓) |
52 | 51 | elv 3454 |
. . . . . . . . 9
⊢
(2nd ‘⟨𝑑, 𝑒, 𝑓⟩) = 𝑓 |
53 | 50, 52 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘𝑦) = 𝑓) |
54 | 53 | breq2d 5122 |
. . . . . . 7
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑐𝑇(2nd ‘𝑦) ↔ 𝑐𝑇𝑓)) |
55 | 53 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑐 = (2nd ‘𝑦) ↔ 𝑐 = 𝑓)) |
56 | 54, 55 | orbi12d 918 |
. . . . . 6
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦)) ↔ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))) |
57 | 42, 49, 56 | 3anbi123d 1437 |
. . . . 5
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (((𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ↔ ((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)))) |
58 | | neeq2 3008 |
. . . . 5
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦 ↔ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)) |
59 | 57, 58 | anbi12d 632 |
. . . 4
⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((((𝑎𝑅(1st ‘(1st
‘𝑦)) ∨ 𝑎 = (1st
‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st
‘𝑦)) ∨ 𝑏 = (2nd
‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩))) |
60 | 32, 59 | 3anbi23d 1440 |
. . 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 5505 |
. 2
⊢
(⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ (⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩))) |
63 | | otelxp 5681 |
. . 3
⊢
(⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) |
64 | | otelxp 5681 |
. . 3
⊢
(⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) |
65 | 5, 6, 7 | otthne 5448 |
. . . 4
⊢
(⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩ ↔ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) |
66 | 65 | anbi2i 624 |
. . 3
⊢ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))) |
67 | 63, 64, 66 | 3anbi123i 1156 |
. 2
⊢
((⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))) |
68 | 62, 67 | bitri 275 |
1
⊢
(⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))) |