Proof of Theorem el2xptp0
Step | Hyp | Ref
| Expression |
1 | | xp1st 7089 |
. . . . . 6
⊢ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) → (1st ‘𝐴) ∈ (𝑈 × 𝑉)) |
2 | 1 | ad2antrl 760 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) → (1st ‘𝐴) ∈ (𝑈 × 𝑉)) |
3 | | 3simpa 1051 |
. . . . . . 7
⊢
(((1st ‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍) → ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌)) |
4 | 3 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍)) → ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌)) |
5 | 4 | adantl 481 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) → ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌)) |
6 | | eqopi 7093 |
. . . . 5
⊢
(((1st ‘𝐴) ∈ (𝑈 × 𝑉) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌)) → (1st ‘𝐴) = 〈𝑋, 𝑌〉) |
7 | 2, 5, 6 | syl2anc 691 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) → (1st ‘𝐴) = 〈𝑋, 𝑌〉) |
8 | | simprr3 1104 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) → (2nd ‘𝐴) = 𝑍) |
9 | 7, 8 | jca 553 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) → ((1st ‘𝐴) = 〈𝑋, 𝑌〉 ∧ (2nd ‘𝐴) = 𝑍)) |
10 | | df-ot 4134 |
. . . . . 6
⊢
〈𝑋, 𝑌, 𝑍〉 = 〈〈𝑋, 𝑌〉, 𝑍〉 |
11 | 10 | eqeq2i 2622 |
. . . . 5
⊢ (𝐴 = 〈𝑋, 𝑌, 𝑍〉 ↔ 𝐴 = 〈〈𝑋, 𝑌〉, 𝑍〉) |
12 | | eqop 7099 |
. . . . 5
⊢ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) → (𝐴 = 〈〈𝑋, 𝑌〉, 𝑍〉 ↔ ((1st ‘𝐴) = 〈𝑋, 𝑌〉 ∧ (2nd ‘𝐴) = 𝑍))) |
13 | 11, 12 | syl5bb 271 |
. . . 4
⊢ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) → (𝐴 = 〈𝑋, 𝑌, 𝑍〉 ↔ ((1st ‘𝐴) = 〈𝑋, 𝑌〉 ∧ (2nd ‘𝐴) = 𝑍))) |
14 | 13 | ad2antrl 760 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) → (𝐴 = 〈𝑋, 𝑌, 𝑍〉 ↔ ((1st ‘𝐴) = 〈𝑋, 𝑌〉 ∧ (2nd ‘𝐴) = 𝑍))) |
15 | 9, 14 | mpbird 246 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) → 𝐴 = 〈𝑋, 𝑌, 𝑍〉) |
16 | | opelxpi 5072 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → 〈𝑋, 𝑌〉 ∈ (𝑈 × 𝑉)) |
17 | 16 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 〈𝑋, 𝑌〉 ∈ (𝑈 × 𝑉)) |
18 | | simp3 1056 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑍 ∈ 𝑊) |
19 | | opelxp 5070 |
. . . . . . 7
⊢
(〈〈𝑋,
𝑌〉, 𝑍〉 ∈ ((𝑈 × 𝑉) × 𝑊) ↔ (〈𝑋, 𝑌〉 ∈ (𝑈 × 𝑉) ∧ 𝑍 ∈ 𝑊)) |
20 | 17, 18, 19 | sylanbrc 695 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 〈〈𝑋, 𝑌〉, 𝑍〉 ∈ ((𝑈 × 𝑉) × 𝑊)) |
21 | 10, 20 | syl5eqel 2692 |
. . . . 5
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 〈𝑋, 𝑌, 𝑍〉 ∈ ((𝑈 × 𝑉) × 𝑊)) |
22 | 21 | adantr 480 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = 〈𝑋, 𝑌, 𝑍〉) → 〈𝑋, 𝑌, 𝑍〉 ∈ ((𝑈 × 𝑉) × 𝑊)) |
23 | | eleq1 2676 |
. . . . 5
⊢ (𝐴 = 〈𝑋, 𝑌, 𝑍〉 → (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ↔ 〈𝑋, 𝑌, 𝑍〉 ∈ ((𝑈 × 𝑉) × 𝑊))) |
24 | 23 | adantl 481 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = 〈𝑋, 𝑌, 𝑍〉) → (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ↔ 〈𝑋, 𝑌, 𝑍〉 ∈ ((𝑈 × 𝑉) × 𝑊))) |
25 | 22, 24 | mpbird 246 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = 〈𝑋, 𝑌, 𝑍〉) → 𝐴 ∈ ((𝑈 × 𝑉) × 𝑊)) |
26 | | fveq2 6103 |
. . . . . 6
⊢ (𝐴 = 〈𝑋, 𝑌, 𝑍〉 → (1st ‘𝐴) = (1st
‘〈𝑋, 𝑌, 𝑍〉)) |
27 | 26 | fveq2d 6107 |
. . . . 5
⊢ (𝐴 = 〈𝑋, 𝑌, 𝑍〉 → (1st
‘(1st ‘𝐴)) = (1st ‘(1st
‘〈𝑋, 𝑌, 𝑍〉))) |
28 | | ot1stg 7073 |
. . . . 5
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (1st
‘(1st ‘〈𝑋, 𝑌, 𝑍〉)) = 𝑋) |
29 | 27, 28 | sylan9eqr 2666 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = 〈𝑋, 𝑌, 𝑍〉) → (1st
‘(1st ‘𝐴)) = 𝑋) |
30 | 26 | fveq2d 6107 |
. . . . 5
⊢ (𝐴 = 〈𝑋, 𝑌, 𝑍〉 → (2nd
‘(1st ‘𝐴)) = (2nd ‘(1st
‘〈𝑋, 𝑌, 𝑍〉))) |
31 | | ot2ndg 7074 |
. . . . 5
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (2nd
‘(1st ‘〈𝑋, 𝑌, 𝑍〉)) = 𝑌) |
32 | 30, 31 | sylan9eqr 2666 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = 〈𝑋, 𝑌, 𝑍〉) → (2nd
‘(1st ‘𝐴)) = 𝑌) |
33 | | fveq2 6103 |
. . . . 5
⊢ (𝐴 = 〈𝑋, 𝑌, 𝑍〉 → (2nd ‘𝐴) = (2nd
‘〈𝑋, 𝑌, 𝑍〉)) |
34 | | ot3rdg 7075 |
. . . . . 6
⊢ (𝑍 ∈ 𝑊 → (2nd ‘〈𝑋, 𝑌, 𝑍〉) = 𝑍) |
35 | 34 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (2nd ‘〈𝑋, 𝑌, 𝑍〉) = 𝑍) |
36 | 33, 35 | sylan9eqr 2666 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = 〈𝑋, 𝑌, 𝑍〉) → (2nd ‘𝐴) = 𝑍) |
37 | 29, 32, 36 | 3jca 1235 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = 〈𝑋, 𝑌, 𝑍〉) → ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍)) |
38 | 25, 37 | jca 553 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝐴 = 〈𝑋, 𝑌, 𝑍〉) → (𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍))) |
39 | 15, 38 | impbida 873 |
1
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st
‘(1st ‘𝐴)) = 𝑋 ∧ (2nd
‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍)) ↔ 𝐴 = 〈𝑋, 𝑌, 𝑍〉)) |