Step | Hyp | Ref
| Expression |
1 | | xp1st 8007 |
. . . . . 6
⊢ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) → (1st ‘𝐴) ∈ (𝑈 × 𝑉)) |
2 | 1 | ad2antrl 727 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) → (1st ‘𝐴) ∈ (𝑈 × 𝑉)) |
3 | | 3simpa 1149 |
. . . . . . 7
⊢
(((1st ‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍) → ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌)) |
4 | 3 | adantl 483 |
. . . . . 6
⊢ ((𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍)) → ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌)) |
5 | 4 | adantl 483 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) → ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌)) |
6 | | eqopi 8011 |
. . . . 5
⊢
(((1st ‘𝐴) ∈ (𝑈 × 𝑉) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌)) → (1st ‘𝐴) = ⟨𝑋, 𝑌⟩) |
7 | 2, 5, 6 | syl2anc 585 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) → (1st ‘𝐴) = ⟨𝑋, 𝑌⟩) |
8 | | simprr3 1224 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) → (2nd ‘𝐴) = 𝑍) |
9 | 7, 8 | jca 513 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) → ((1st ‘𝐴) = ⟨𝑋, 𝑌⟩ ∧ (2nd ‘𝐴) = 𝑍)) |
10 | | df-ot 4638 |
. . . . . 6
⊢
⟨𝑋, 𝑌, 𝑍⟩ = ⟨⟨𝑋, 𝑌⟩, 𝑍⟩ |
11 | 10 | eqeq2i 2746 |
. . . . 5
⊢ (𝐴 = ⟨𝑋, 𝑌, 𝑍⟩ ↔ 𝐴 = ⟨⟨𝑋, 𝑌⟩, 𝑍⟩) |
12 | | eqop 8017 |
. . . . 5
⊢ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) → (𝐴 = ⟨⟨𝑋, 𝑌⟩, 𝑍⟩ ↔ ((1st ‘𝐴) = ⟨𝑋, 𝑌⟩ ∧ (2nd ‘𝐴) = 𝑍))) |
13 | 11, 12 | bitrid 283 |
. . . 4
⊢ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) → (𝐴 = ⟨𝑋, 𝑌, 𝑍⟩ ↔ ((1st ‘𝐴) = ⟨𝑋, 𝑌⟩ ∧ (2nd ‘𝐴) = 𝑍))) |
14 | 13 | ad2antrl 727 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) → (𝐴 = ⟨𝑋, 𝑌, 𝑍⟩ ↔ ((1st ‘𝐴) = ⟨𝑋, 𝑌⟩ ∧ (2nd ‘𝐴) = 𝑍))) |
15 | 9, 14 | mpbird 257 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) → 𝐴 = ⟨𝑋, 𝑌, 𝑍⟩) |
16 | | opelxpi 5714 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → ⟨𝑋, 𝑌⟩ ∈ (𝑈 × 𝑉)) |
17 | 16 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ⟨𝑋, 𝑌⟩ ∈ (𝑈 × 𝑉)) |
18 | | simp3 1139 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑍 ∈ 𝑊) |
19 | 17, 18 | opelxpd 5716 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ⟨⟨𝑋, 𝑌⟩, 𝑍⟩ ∈ ((𝑈 × 𝑉) × 𝑊)) |
20 | 10, 19 | eqeltrid 2838 |
. . . . 5
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ⟨𝑋, 𝑌, 𝑍⟩ ∈ ((𝑈 × 𝑉) × 𝑊)) |
21 | 20 | adantr 482 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = ⟨𝑋, 𝑌, 𝑍⟩) → ⟨𝑋, 𝑌, 𝑍⟩ ∈ ((𝑈 × 𝑉) × 𝑊)) |
22 | | eleq1 2822 |
. . . . 5
⊢ (𝐴 = ⟨𝑋, 𝑌, 𝑍⟩ → (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ↔ ⟨𝑋, 𝑌, 𝑍⟩ ∈ ((𝑈 × 𝑉) × 𝑊))) |
23 | 22 | adantl 483 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = ⟨𝑋, 𝑌, 𝑍⟩) → (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ↔ ⟨𝑋, 𝑌, 𝑍⟩ ∈ ((𝑈 × 𝑉) × 𝑊))) |
24 | 21, 23 | mpbird 257 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = ⟨𝑋, 𝑌, 𝑍⟩) → 𝐴 ∈ ((𝑈 × 𝑉) × 𝑊)) |
25 | | 2fveq3 6897 |
. . . . 5
⊢ (𝐴 = ⟨𝑋, 𝑌, 𝑍⟩ → (1st
‘(1st ‘𝐴)) = (1st ‘(1st
‘⟨𝑋, 𝑌, 𝑍⟩))) |
26 | | ot1stg 7989 |
. . . . 5
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (1st
‘(1st ‘⟨𝑋, 𝑌, 𝑍⟩)) = 𝑋) |
27 | 25, 26 | sylan9eqr 2795 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = ⟨𝑋, 𝑌, 𝑍⟩) → (1st
‘(1st ‘𝐴)) = 𝑋) |
28 | | 2fveq3 6897 |
. . . . 5
⊢ (𝐴 = ⟨𝑋, 𝑌, 𝑍⟩ → (2nd
‘(1st ‘𝐴)) = (2nd ‘(1st
‘⟨𝑋, 𝑌, 𝑍⟩))) |
29 | | ot2ndg 7990 |
. . . . 5
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (2nd
‘(1st ‘⟨𝑋, 𝑌, 𝑍⟩)) = 𝑌) |
30 | 28, 29 | sylan9eqr 2795 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = ⟨𝑋, 𝑌, 𝑍⟩) → (2nd
‘(1st ‘𝐴)) = 𝑌) |
31 | | fveq2 6892 |
. . . . 5
⊢ (𝐴 = ⟨𝑋, 𝑌, 𝑍⟩ → (2nd ‘𝐴) = (2nd
‘⟨𝑋, 𝑌, 𝑍⟩)) |
32 | | ot3rdg 7991 |
. . . . . 6
⊢ (𝑍 ∈ 𝑊 → (2nd ‘⟨𝑋, 𝑌, 𝑍⟩) = 𝑍) |
33 | 32 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (2nd ‘⟨𝑋, 𝑌, 𝑍⟩) = 𝑍) |
34 | 31, 33 | sylan9eqr 2795 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = ⟨𝑋, 𝑌, 𝑍⟩) → (2nd ‘𝐴) = 𝑍) |
35 | 27, 30, 34 | 3jca 1129 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = ⟨𝑋, 𝑌, 𝑍⟩) → ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍)) |
36 | 24, 35 | jca 513 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = ⟨𝑋, 𝑌, 𝑍⟩) → (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) |
37 | 15, 36 | impbida 800 |
1
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍)) ↔ 𝐴 = ⟨𝑋, 𝑌, 𝑍⟩)) |