Proof of Theorem xpmapenlem
Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. 2
⊢ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∈ V |
2 | | ovex 6678 |
. . 3
⊢ (𝐴 ↑𝑚
𝐶) ∈
V |
3 | | ovex 6678 |
. . 3
⊢ (𝐵 ↑𝑚
𝐶) ∈
V |
4 | 2, 3 | xpex 6962 |
. 2
⊢ ((𝐴 ↑𝑚
𝐶) × (𝐵 ↑𝑚
𝐶)) ∈
V |
5 | | xpmapen.1 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
6 | | xpmapen.2 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
7 | 5, 6 | xpex 6962 |
. . . . . . . 8
⊢ (𝐴 × 𝐵) ∈ V |
8 | | xpmapen.3 |
. . . . . . . 8
⊢ 𝐶 ∈ V |
9 | 7, 8 | elmap 7886 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ↔ 𝑥:𝐶⟶(𝐴 × 𝐵)) |
10 | | ffvelrn 6357 |
. . . . . . 7
⊢ ((𝑥:𝐶⟶(𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) ∈ (𝐴 × 𝐵)) |
11 | 9, 10 | sylanb 489 |
. . . . . 6
⊢ ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) ∈ (𝐴 × 𝐵)) |
12 | | xp1st 7198 |
. . . . . 6
⊢ ((𝑥‘𝑧) ∈ (𝐴 × 𝐵) → (1st ‘(𝑥‘𝑧)) ∈ 𝐴) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑧 ∈ 𝐶) → (1st ‘(𝑥‘𝑧)) ∈ 𝐴) |
14 | | xpmapenlem.4 |
. . . . 5
⊢ 𝐷 = (𝑧 ∈ 𝐶 ↦ (1st ‘(𝑥‘𝑧))) |
15 | 13, 14 | fmptd 6385 |
. . . 4
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝐷:𝐶⟶𝐴) |
16 | 5, 8 | elmap 7886 |
. . . 4
⊢ (𝐷 ∈ (𝐴 ↑𝑚 𝐶) ↔ 𝐷:𝐶⟶𝐴) |
17 | 15, 16 | sylibr 224 |
. . 3
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝐷 ∈ (𝐴 ↑𝑚 𝐶)) |
18 | | xp2nd 7199 |
. . . . . 6
⊢ ((𝑥‘𝑧) ∈ (𝐴 × 𝐵) → (2nd ‘(𝑥‘𝑧)) ∈ 𝐵) |
19 | 11, 18 | syl 17 |
. . . . 5
⊢ ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑧 ∈ 𝐶) → (2nd ‘(𝑥‘𝑧)) ∈ 𝐵) |
20 | | xpmapenlem.5 |
. . . . 5
⊢ 𝑅 = (𝑧 ∈ 𝐶 ↦ (2nd ‘(𝑥‘𝑧))) |
21 | 19, 20 | fmptd 6385 |
. . . 4
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝑅:𝐶⟶𝐵) |
22 | 6, 8 | elmap 7886 |
. . . 4
⊢ (𝑅 ∈ (𝐵 ↑𝑚 𝐶) ↔ 𝑅:𝐶⟶𝐵) |
23 | 21, 22 | sylibr 224 |
. . 3
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 𝑅 ∈ (𝐵 ↑𝑚 𝐶)) |
24 | | opelxpi 5148 |
. . 3
⊢ ((𝐷 ∈ (𝐴 ↑𝑚 𝐶) ∧ 𝑅 ∈ (𝐵 ↑𝑚 𝐶)) → 〈𝐷, 𝑅〉 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) |
25 | 17, 23, 24 | syl2anc 693 |
. 2
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) → 〈𝐷, 𝑅〉 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) |
26 | | xp1st 7198 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) → (1st
‘𝑦) ∈ (𝐴 ↑𝑚
𝐶)) |
27 | 5, 8 | elmap 7886 |
. . . . . . 7
⊢
((1st ‘𝑦) ∈ (𝐴 ↑𝑚 𝐶) ↔ (1st
‘𝑦):𝐶⟶𝐴) |
28 | 26, 27 | sylib 208 |
. . . . . 6
⊢ (𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) → (1st
‘𝑦):𝐶⟶𝐴) |
29 | 28 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) ∧ 𝑧 ∈ 𝐶) → ((1st ‘𝑦)‘𝑧) ∈ 𝐴) |
30 | | xp2nd 7199 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) → (2nd
‘𝑦) ∈ (𝐵 ↑𝑚
𝐶)) |
31 | 6, 8 | elmap 7886 |
. . . . . . 7
⊢
((2nd ‘𝑦) ∈ (𝐵 ↑𝑚 𝐶) ↔ (2nd
‘𝑦):𝐶⟶𝐵) |
32 | 30, 31 | sylib 208 |
. . . . . 6
⊢ (𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) → (2nd
‘𝑦):𝐶⟶𝐵) |
33 | 32 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) ∧ 𝑧 ∈ 𝐶) → ((2nd ‘𝑦)‘𝑧) ∈ 𝐵) |
34 | | opelxpi 5148 |
. . . . 5
⊢
((((1st ‘𝑦)‘𝑧) ∈ 𝐴 ∧ ((2nd ‘𝑦)‘𝑧) ∈ 𝐵) → 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉 ∈ (𝐴 × 𝐵)) |
35 | 29, 33, 34 | syl2anc 693 |
. . . 4
⊢ ((𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) ∧ 𝑧 ∈ 𝐶) → 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉 ∈ (𝐴 × 𝐵)) |
36 | | xpmapenlem.6 |
. . . 4
⊢ 𝑆 = (𝑧 ∈ 𝐶 ↦ 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) |
37 | 35, 36 | fmptd 6385 |
. . 3
⊢ (𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) → 𝑆:𝐶⟶(𝐴 × 𝐵)) |
38 | 7, 8 | elmap 7886 |
. . 3
⊢ (𝑆 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ↔ 𝑆:𝐶⟶(𝐴 × 𝐵)) |
39 | 37, 38 | sylibr 224 |
. 2
⊢ (𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) → 𝑆 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶)) |
40 | | 1st2nd2 7205 |
. . . . 5
⊢ (𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
41 | 40 | ad2antlr 763 |
. . . 4
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
42 | 28 | feqmptd 6249 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) → (1st
‘𝑦) = (𝑧 ∈ 𝐶 ↦ ((1st ‘𝑦)‘𝑧))) |
43 | 42 | ad2antlr 763 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (1st ‘𝑦) = (𝑧 ∈ 𝐶 ↦ ((1st ‘𝑦)‘𝑧))) |
44 | | simplr 792 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → 𝑥 = 𝑆) |
45 | 44 | fveq1d 6193 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) = (𝑆‘𝑧)) |
46 | | opex 4932 |
. . . . . . . . . . . . 13
⊢
〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉 ∈ V |
47 | 36 | fvmpt2 6291 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐶 ∧ 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉 ∈ V) → (𝑆‘𝑧) = 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) |
48 | 46, 47 | mpan2 707 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝐶 → (𝑆‘𝑧) = 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) |
49 | 48 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (𝑆‘𝑧) = 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) |
50 | 45, 49 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) = 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) |
51 | 50 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (1st ‘(𝑥‘𝑧)) = (1st
‘〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉)) |
52 | | fvex 6201 |
. . . . . . . . . 10
⊢
((1st ‘𝑦)‘𝑧) ∈ V |
53 | | fvex 6201 |
. . . . . . . . . 10
⊢
((2nd ‘𝑦)‘𝑧) ∈ V |
54 | 52, 53 | op1st 7176 |
. . . . . . . . 9
⊢
(1st ‘〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) = ((1st ‘𝑦)‘𝑧) |
55 | 51, 54 | syl6eq 2672 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (1st ‘(𝑥‘𝑧)) = ((1st ‘𝑦)‘𝑧)) |
56 | 55 | mpteq2dva 4744 |
. . . . . . 7
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (𝑧 ∈ 𝐶 ↦ (1st ‘(𝑥‘𝑧))) = (𝑧 ∈ 𝐶 ↦ ((1st ‘𝑦)‘𝑧))) |
57 | 14, 56 | syl5eq 2668 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝐷 = (𝑧 ∈ 𝐶 ↦ ((1st ‘𝑦)‘𝑧))) |
58 | 43, 57 | eqtr4d 2659 |
. . . . 5
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (1st ‘𝑦) = 𝐷) |
59 | 32 | feqmptd 6249 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) → (2nd
‘𝑦) = (𝑧 ∈ 𝐶 ↦ ((2nd ‘𝑦)‘𝑧))) |
60 | 59 | ad2antlr 763 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (2nd ‘𝑦) = (𝑧 ∈ 𝐶 ↦ ((2nd ‘𝑦)‘𝑧))) |
61 | 50 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (2nd ‘(𝑥‘𝑧)) = (2nd
‘〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉)) |
62 | 52, 53 | op2nd 7177 |
. . . . . . . . 9
⊢
(2nd ‘〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) = ((2nd ‘𝑦)‘𝑧) |
63 | 61, 62 | syl6eq 2672 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (2nd ‘(𝑥‘𝑧)) = ((2nd ‘𝑦)‘𝑧)) |
64 | 63 | mpteq2dva 4744 |
. . . . . . 7
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (𝑧 ∈ 𝐶 ↦ (2nd ‘(𝑥‘𝑧))) = (𝑧 ∈ 𝐶 ↦ ((2nd ‘𝑦)‘𝑧))) |
65 | 20, 64 | syl5eq 2668 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝑅 = (𝑧 ∈ 𝐶 ↦ ((2nd ‘𝑦)‘𝑧))) |
66 | 60, 65 | eqtr4d 2659 |
. . . . 5
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) → (2nd ‘𝑦) = 𝑅) |
67 | 58, 66 | opeq12d 4410 |
. . . 4
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈𝐷, 𝑅〉) |
68 | 41, 67 | eqtrd 2656 |
. . 3
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑥 = 𝑆) → 𝑦 = 〈𝐷, 𝑅〉) |
69 | | simpll 790 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶)) |
70 | 69, 9 | sylib 208 |
. . . . 5
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝑥:𝐶⟶(𝐴 × 𝐵)) |
71 | 70 | feqmptd 6249 |
. . . 4
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝑥 = (𝑧 ∈ 𝐶 ↦ (𝑥‘𝑧))) |
72 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝑦 = 〈𝐷, 𝑅〉) |
73 | 72 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → (1st ‘𝑦) = (1st
‘〈𝐷, 𝑅〉)) |
74 | 17 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝐷 ∈ (𝐴 ↑𝑚 𝐶)) |
75 | 23 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝑅 ∈ (𝐵 ↑𝑚 𝐶)) |
76 | | op1stg 7180 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (𝐴 ↑𝑚 𝐶) ∧ 𝑅 ∈ (𝐵 ↑𝑚 𝐶)) → (1st
‘〈𝐷, 𝑅〉) = 𝐷) |
77 | 74, 75, 76 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → (1st
‘〈𝐷, 𝑅〉) = 𝐷) |
78 | 73, 77 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → (1st ‘𝑦) = 𝐷) |
79 | 78 | fveq1d 6193 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → ((1st ‘𝑦)‘𝑧) = (𝐷‘𝑧)) |
80 | | fvex 6201 |
. . . . . . . . . 10
⊢
(1st ‘(𝑥‘𝑧)) ∈ V |
81 | 14 | fvmpt2 6291 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐶 ∧ (1st ‘(𝑥‘𝑧)) ∈ V) → (𝐷‘𝑧) = (1st ‘(𝑥‘𝑧))) |
82 | 80, 81 | mpan2 707 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐶 → (𝐷‘𝑧) = (1st ‘(𝑥‘𝑧))) |
83 | 79, 82 | sylan9eq 2676 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) ∧ 𝑧 ∈ 𝐶) → ((1st ‘𝑦)‘𝑧) = (1st ‘(𝑥‘𝑧))) |
84 | 72 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → (2nd ‘𝑦) = (2nd
‘〈𝐷, 𝑅〉)) |
85 | | op2ndg 7181 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (𝐴 ↑𝑚 𝐶) ∧ 𝑅 ∈ (𝐵 ↑𝑚 𝐶)) → (2nd
‘〈𝐷, 𝑅〉) = 𝑅) |
86 | 74, 75, 85 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → (2nd
‘〈𝐷, 𝑅〉) = 𝑅) |
87 | 84, 86 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → (2nd ‘𝑦) = 𝑅) |
88 | 87 | fveq1d 6193 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → ((2nd ‘𝑦)‘𝑧) = (𝑅‘𝑧)) |
89 | | fvex 6201 |
. . . . . . . . . 10
⊢
(2nd ‘(𝑥‘𝑧)) ∈ V |
90 | 20 | fvmpt2 6291 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐶 ∧ (2nd ‘(𝑥‘𝑧)) ∈ V) → (𝑅‘𝑧) = (2nd ‘(𝑥‘𝑧))) |
91 | 89, 90 | mpan2 707 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐶 → (𝑅‘𝑧) = (2nd ‘(𝑥‘𝑧))) |
92 | 88, 91 | sylan9eq 2676 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) ∧ 𝑧 ∈ 𝐶) → ((2nd ‘𝑦)‘𝑧) = (2nd ‘(𝑥‘𝑧))) |
93 | 83, 92 | opeq12d 4410 |
. . . . . . 7
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) ∧ 𝑧 ∈ 𝐶) → 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉 = 〈(1st ‘(𝑥‘𝑧)), (2nd ‘(𝑥‘𝑧))〉) |
94 | 70 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) ∈ (𝐴 × 𝐵)) |
95 | | 1st2nd2 7205 |
. . . . . . . 8
⊢ ((𝑥‘𝑧) ∈ (𝐴 × 𝐵) → (𝑥‘𝑧) = 〈(1st ‘(𝑥‘𝑧)), (2nd ‘(𝑥‘𝑧))〉) |
96 | 94, 95 | syl 17 |
. . . . . . 7
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) = 〈(1st ‘(𝑥‘𝑧)), (2nd ‘(𝑥‘𝑧))〉) |
97 | 93, 96 | eqtr4d 2659 |
. . . . . 6
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) ∧ 𝑧 ∈ 𝐶) → 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉 = (𝑥‘𝑧)) |
98 | 97 | mpteq2dva 4744 |
. . . . 5
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → (𝑧 ∈ 𝐶 ↦ 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) = (𝑧 ∈ 𝐶 ↦ (𝑥‘𝑧))) |
99 | 36, 98 | syl5eq 2668 |
. . . 4
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝑆 = (𝑧 ∈ 𝐶 ↦ (𝑥‘𝑧))) |
100 | 71, 99 | eqtr4d 2659 |
. . 3
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝑥 = 𝑆) |
101 | 68, 100 | impbida 877 |
. 2
⊢ ((𝑥 ∈ ((𝐴 × 𝐵) ↑𝑚 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶))) → (𝑥 = 𝑆 ↔ 𝑦 = 〈𝐷, 𝑅〉)) |
102 | 1, 4, 25, 39, 101 | en3i 7994 |
1
⊢ ((𝐴 × 𝐵) ↑𝑚 𝐶) ≈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) |