Proof of Theorem xpmapenlem
Step | Hyp | Ref
| Expression |
1 | | ovex 7308 |
. 2
⊢ ((𝐴 × 𝐵) ↑m 𝐶) ∈ V |
2 | | ovex 7308 |
. . 3
⊢ (𝐴 ↑m 𝐶) ∈ V |
3 | | ovex 7308 |
. . 3
⊢ (𝐵 ↑m 𝐶) ∈ V |
4 | 2, 3 | xpex 7603 |
. 2
⊢ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) ∈ V |
5 | | xpmapen.1 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
6 | | xpmapen.2 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
7 | 5, 6 | xpex 7603 |
. . . . . . . 8
⊢ (𝐴 × 𝐵) ∈ V |
8 | | xpmapen.3 |
. . . . . . . 8
⊢ 𝐶 ∈ V |
9 | 7, 8 | elmap 8659 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ↔ 𝑥:𝐶⟶(𝐴 × 𝐵)) |
10 | | ffvelrn 6959 |
. . . . . . 7
⊢ ((𝑥:𝐶⟶(𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) ∈ (𝐴 × 𝐵)) |
11 | 9, 10 | sylanb 581 |
. . . . . 6
⊢ ((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) ∈ (𝐴 × 𝐵)) |
12 | | xp1st 7863 |
. . . . . 6
⊢ ((𝑥‘𝑧) ∈ (𝐴 × 𝐵) → (1st ‘(𝑥‘𝑧)) ∈ 𝐴) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ ((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑧 ∈ 𝐶) → (1st ‘(𝑥‘𝑧)) ∈ 𝐴) |
14 | | xpmapenlem.4 |
. . . . 5
⊢ 𝐷 = (𝑧 ∈ 𝐶 ↦ (1st ‘(𝑥‘𝑧))) |
15 | 13, 14 | fmptd 6988 |
. . . 4
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) → 𝐷:𝐶⟶𝐴) |
16 | 5, 8 | elmap 8659 |
. . . 4
⊢ (𝐷 ∈ (𝐴 ↑m 𝐶) ↔ 𝐷:𝐶⟶𝐴) |
17 | 15, 16 | sylibr 233 |
. . 3
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) → 𝐷 ∈ (𝐴 ↑m 𝐶)) |
18 | | xp2nd 7864 |
. . . . . 6
⊢ ((𝑥‘𝑧) ∈ (𝐴 × 𝐵) → (2nd ‘(𝑥‘𝑧)) ∈ 𝐵) |
19 | 11, 18 | syl 17 |
. . . . 5
⊢ ((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑧 ∈ 𝐶) → (2nd ‘(𝑥‘𝑧)) ∈ 𝐵) |
20 | | xpmapenlem.5 |
. . . . 5
⊢ 𝑅 = (𝑧 ∈ 𝐶 ↦ (2nd ‘(𝑥‘𝑧))) |
21 | 19, 20 | fmptd 6988 |
. . . 4
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) → 𝑅:𝐶⟶𝐵) |
22 | 6, 8 | elmap 8659 |
. . . 4
⊢ (𝑅 ∈ (𝐵 ↑m 𝐶) ↔ 𝑅:𝐶⟶𝐵) |
23 | 21, 22 | sylibr 233 |
. . 3
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) → 𝑅 ∈ (𝐵 ↑m 𝐶)) |
24 | 17, 23 | opelxpd 5627 |
. 2
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) → 〈𝐷, 𝑅〉 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) |
25 | | xp1st 7863 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → (1st ‘𝑦) ∈ (𝐴 ↑m 𝐶)) |
26 | 5, 8 | elmap 8659 |
. . . . . . 7
⊢
((1st ‘𝑦) ∈ (𝐴 ↑m 𝐶) ↔ (1st ‘𝑦):𝐶⟶𝐴) |
27 | 25, 26 | sylib 217 |
. . . . . 6
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → (1st ‘𝑦):𝐶⟶𝐴) |
28 | 27 | ffvelrnda 6961 |
. . . . 5
⊢ ((𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) ∧ 𝑧 ∈ 𝐶) → ((1st ‘𝑦)‘𝑧) ∈ 𝐴) |
29 | | xp2nd 7864 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → (2nd ‘𝑦) ∈ (𝐵 ↑m 𝐶)) |
30 | 6, 8 | elmap 8659 |
. . . . . . 7
⊢
((2nd ‘𝑦) ∈ (𝐵 ↑m 𝐶) ↔ (2nd ‘𝑦):𝐶⟶𝐵) |
31 | 29, 30 | sylib 217 |
. . . . . 6
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → (2nd ‘𝑦):𝐶⟶𝐵) |
32 | 31 | ffvelrnda 6961 |
. . . . 5
⊢ ((𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) ∧ 𝑧 ∈ 𝐶) → ((2nd ‘𝑦)‘𝑧) ∈ 𝐵) |
33 | 28, 32 | opelxpd 5627 |
. . . 4
⊢ ((𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) ∧ 𝑧 ∈ 𝐶) → 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉 ∈ (𝐴 × 𝐵)) |
34 | | xpmapenlem.6 |
. . . 4
⊢ 𝑆 = (𝑧 ∈ 𝐶 ↦ 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) |
35 | 33, 34 | fmptd 6988 |
. . 3
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → 𝑆:𝐶⟶(𝐴 × 𝐵)) |
36 | 7, 8 | elmap 8659 |
. . 3
⊢ (𝑆 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ↔ 𝑆:𝐶⟶(𝐴 × 𝐵)) |
37 | 35, 36 | sylibr 233 |
. 2
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → 𝑆 ∈ ((𝐴 × 𝐵) ↑m 𝐶)) |
38 | | 1st2nd2 7870 |
. . . . 5
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
39 | 38 | ad2antlr 724 |
. . . 4
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
40 | 27 | feqmptd 6837 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → (1st ‘𝑦) = (𝑧 ∈ 𝐶 ↦ ((1st ‘𝑦)‘𝑧))) |
41 | 40 | ad2antlr 724 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → (1st ‘𝑦) = (𝑧 ∈ 𝐶 ↦ ((1st ‘𝑦)‘𝑧))) |
42 | | simplr 766 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → 𝑥 = 𝑆) |
43 | 42 | fveq1d 6776 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) = (𝑆‘𝑧)) |
44 | | opex 5379 |
. . . . . . . . . . . . 13
⊢
〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉 ∈ V |
45 | 34 | fvmpt2 6886 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐶 ∧ 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉 ∈ V) → (𝑆‘𝑧) = 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) |
46 | 44, 45 | mpan2 688 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝐶 → (𝑆‘𝑧) = 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) |
47 | 46 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (𝑆‘𝑧) = 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) |
48 | 43, 47 | eqtrd 2778 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) = 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) |
49 | 48 | fveq2d 6778 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (1st ‘(𝑥‘𝑧)) = (1st
‘〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉)) |
50 | | fvex 6787 |
. . . . . . . . . 10
⊢
((1st ‘𝑦)‘𝑧) ∈ V |
51 | | fvex 6787 |
. . . . . . . . . 10
⊢
((2nd ‘𝑦)‘𝑧) ∈ V |
52 | 50, 51 | op1st 7839 |
. . . . . . . . 9
⊢
(1st ‘〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) = ((1st ‘𝑦)‘𝑧) |
53 | 49, 52 | eqtrdi 2794 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (1st ‘(𝑥‘𝑧)) = ((1st ‘𝑦)‘𝑧)) |
54 | 53 | mpteq2dva 5174 |
. . . . . . 7
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → (𝑧 ∈ 𝐶 ↦ (1st ‘(𝑥‘𝑧))) = (𝑧 ∈ 𝐶 ↦ ((1st ‘𝑦)‘𝑧))) |
55 | 14, 54 | eqtrid 2790 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → 𝐷 = (𝑧 ∈ 𝐶 ↦ ((1st ‘𝑦)‘𝑧))) |
56 | 41, 55 | eqtr4d 2781 |
. . . . 5
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → (1st ‘𝑦) = 𝐷) |
57 | 31 | feqmptd 6837 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → (2nd ‘𝑦) = (𝑧 ∈ 𝐶 ↦ ((2nd ‘𝑦)‘𝑧))) |
58 | 57 | ad2antlr 724 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → (2nd ‘𝑦) = (𝑧 ∈ 𝐶 ↦ ((2nd ‘𝑦)‘𝑧))) |
59 | 48 | fveq2d 6778 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (2nd ‘(𝑥‘𝑧)) = (2nd
‘〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉)) |
60 | 50, 51 | op2nd 7840 |
. . . . . . . . 9
⊢
(2nd ‘〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) = ((2nd ‘𝑦)‘𝑧) |
61 | 59, 60 | eqtrdi 2794 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (2nd ‘(𝑥‘𝑧)) = ((2nd ‘𝑦)‘𝑧)) |
62 | 61 | mpteq2dva 5174 |
. . . . . . 7
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → (𝑧 ∈ 𝐶 ↦ (2nd ‘(𝑥‘𝑧))) = (𝑧 ∈ 𝐶 ↦ ((2nd ‘𝑦)‘𝑧))) |
63 | 20, 62 | eqtrid 2790 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → 𝑅 = (𝑧 ∈ 𝐶 ↦ ((2nd ‘𝑦)‘𝑧))) |
64 | 58, 63 | eqtr4d 2781 |
. . . . 5
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → (2nd ‘𝑦) = 𝑅) |
65 | 56, 64 | opeq12d 4812 |
. . . 4
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → 〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈𝐷, 𝑅〉) |
66 | 39, 65 | eqtrd 2778 |
. . 3
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → 𝑦 = 〈𝐷, 𝑅〉) |
67 | | simpll 764 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶)) |
68 | 67, 9 | sylib 217 |
. . . . 5
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝑥:𝐶⟶(𝐴 × 𝐵)) |
69 | 68 | feqmptd 6837 |
. . . 4
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝑥 = (𝑧 ∈ 𝐶 ↦ (𝑥‘𝑧))) |
70 | | simpr 485 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝑦 = 〈𝐷, 𝑅〉) |
71 | 70 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → (1st ‘𝑦) = (1st
‘〈𝐷, 𝑅〉)) |
72 | 17 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝐷 ∈ (𝐴 ↑m 𝐶)) |
73 | 23 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝑅 ∈ (𝐵 ↑m 𝐶)) |
74 | | op1stg 7843 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (𝐴 ↑m 𝐶) ∧ 𝑅 ∈ (𝐵 ↑m 𝐶)) → (1st ‘〈𝐷, 𝑅〉) = 𝐷) |
75 | 72, 73, 74 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → (1st
‘〈𝐷, 𝑅〉) = 𝐷) |
76 | 71, 75 | eqtrd 2778 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → (1st ‘𝑦) = 𝐷) |
77 | 76 | fveq1d 6776 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → ((1st ‘𝑦)‘𝑧) = (𝐷‘𝑧)) |
78 | | fvex 6787 |
. . . . . . . . . 10
⊢
(1st ‘(𝑥‘𝑧)) ∈ V |
79 | 14 | fvmpt2 6886 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐶 ∧ (1st ‘(𝑥‘𝑧)) ∈ V) → (𝐷‘𝑧) = (1st ‘(𝑥‘𝑧))) |
80 | 78, 79 | mpan2 688 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐶 → (𝐷‘𝑧) = (1st ‘(𝑥‘𝑧))) |
81 | 77, 80 | sylan9eq 2798 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) ∧ 𝑧 ∈ 𝐶) → ((1st ‘𝑦)‘𝑧) = (1st ‘(𝑥‘𝑧))) |
82 | 70 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → (2nd ‘𝑦) = (2nd
‘〈𝐷, 𝑅〉)) |
83 | | op2ndg 7844 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (𝐴 ↑m 𝐶) ∧ 𝑅 ∈ (𝐵 ↑m 𝐶)) → (2nd ‘〈𝐷, 𝑅〉) = 𝑅) |
84 | 72, 73, 83 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → (2nd
‘〈𝐷, 𝑅〉) = 𝑅) |
85 | 82, 84 | eqtrd 2778 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → (2nd ‘𝑦) = 𝑅) |
86 | 85 | fveq1d 6776 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → ((2nd ‘𝑦)‘𝑧) = (𝑅‘𝑧)) |
87 | | fvex 6787 |
. . . . . . . . . 10
⊢
(2nd ‘(𝑥‘𝑧)) ∈ V |
88 | 20 | fvmpt2 6886 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐶 ∧ (2nd ‘(𝑥‘𝑧)) ∈ V) → (𝑅‘𝑧) = (2nd ‘(𝑥‘𝑧))) |
89 | 87, 88 | mpan2 688 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐶 → (𝑅‘𝑧) = (2nd ‘(𝑥‘𝑧))) |
90 | 86, 89 | sylan9eq 2798 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) ∧ 𝑧 ∈ 𝐶) → ((2nd ‘𝑦)‘𝑧) = (2nd ‘(𝑥‘𝑧))) |
91 | 81, 90 | opeq12d 4812 |
. . . . . . 7
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) ∧ 𝑧 ∈ 𝐶) → 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉 = 〈(1st ‘(𝑥‘𝑧)), (2nd ‘(𝑥‘𝑧))〉) |
92 | 68 | ffvelrnda 6961 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) ∈ (𝐴 × 𝐵)) |
93 | | 1st2nd2 7870 |
. . . . . . . 8
⊢ ((𝑥‘𝑧) ∈ (𝐴 × 𝐵) → (𝑥‘𝑧) = 〈(1st ‘(𝑥‘𝑧)), (2nd ‘(𝑥‘𝑧))〉) |
94 | 92, 93 | syl 17 |
. . . . . . 7
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) = 〈(1st ‘(𝑥‘𝑧)), (2nd ‘(𝑥‘𝑧))〉) |
95 | 91, 94 | eqtr4d 2781 |
. . . . . 6
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) ∧ 𝑧 ∈ 𝐶) → 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉 = (𝑥‘𝑧)) |
96 | 95 | mpteq2dva 5174 |
. . . . 5
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → (𝑧 ∈ 𝐶 ↦ 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) = (𝑧 ∈ 𝐶 ↦ (𝑥‘𝑧))) |
97 | 34, 96 | eqtrid 2790 |
. . . 4
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝑆 = (𝑧 ∈ 𝐶 ↦ (𝑥‘𝑧))) |
98 | 69, 97 | eqtr4d 2781 |
. . 3
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = 〈𝐷, 𝑅〉) → 𝑥 = 𝑆) |
99 | 66, 98 | impbida 798 |
. 2
⊢ ((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) → (𝑥 = 𝑆 ↔ 𝑦 = 〈𝐷, 𝑅〉)) |
100 | 1, 4, 24, 37, 99 | en3i 8779 |
1
⊢ ((𝐴 × 𝐵) ↑m 𝐶) ≈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) |