Step | Hyp | Ref
| Expression |
1 | | ovex 7391 |
. 2
⊢ ((𝐴 × 𝐵) ↑m 𝐶) ∈ V |
2 | | ovex 7391 |
. . 3
⊢ (𝐴 ↑m 𝐶) ∈ V |
3 | | ovex 7391 |
. . 3
⊢ (𝐵 ↑m 𝐶) ∈ V |
4 | 2, 3 | xpex 7688 |
. 2
⊢ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) ∈ V |
5 | | xpmapen.1 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
6 | | xpmapen.2 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
7 | 5, 6 | xpex 7688 |
. . . . . . . 8
⊢ (𝐴 × 𝐵) ∈ V |
8 | | xpmapen.3 |
. . . . . . . 8
⊢ 𝐶 ∈ V |
9 | 7, 8 | elmap 8812 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ↔ 𝑥:𝐶⟶(𝐴 × 𝐵)) |
10 | | ffvelcdm 7033 |
. . . . . . 7
⊢ ((𝑥:𝐶⟶(𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) ∈ (𝐴 × 𝐵)) |
11 | 9, 10 | sylanb 582 |
. . . . . 6
⊢ ((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) ∈ (𝐴 × 𝐵)) |
12 | | xp1st 7954 |
. . . . . 6
⊢ ((𝑥‘𝑧) ∈ (𝐴 × 𝐵) → (1st ‘(𝑥‘𝑧)) ∈ 𝐴) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ ((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑧 ∈ 𝐶) → (1st ‘(𝑥‘𝑧)) ∈ 𝐴) |
14 | | xpmapenlem.4 |
. . . . 5
⊢ 𝐷 = (𝑧 ∈ 𝐶 ↦ (1st ‘(𝑥‘𝑧))) |
15 | 13, 14 | fmptd 7063 |
. . . 4
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) → 𝐷:𝐶⟶𝐴) |
16 | 5, 8 | elmap 8812 |
. . . 4
⊢ (𝐷 ∈ (𝐴 ↑m 𝐶) ↔ 𝐷:𝐶⟶𝐴) |
17 | 15, 16 | sylibr 233 |
. . 3
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) → 𝐷 ∈ (𝐴 ↑m 𝐶)) |
18 | | xp2nd 7955 |
. . . . . 6
⊢ ((𝑥‘𝑧) ∈ (𝐴 × 𝐵) → (2nd ‘(𝑥‘𝑧)) ∈ 𝐵) |
19 | 11, 18 | syl 17 |
. . . . 5
⊢ ((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑧 ∈ 𝐶) → (2nd ‘(𝑥‘𝑧)) ∈ 𝐵) |
20 | | xpmapenlem.5 |
. . . . 5
⊢ 𝑅 = (𝑧 ∈ 𝐶 ↦ (2nd ‘(𝑥‘𝑧))) |
21 | 19, 20 | fmptd 7063 |
. . . 4
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) → 𝑅:𝐶⟶𝐵) |
22 | 6, 8 | elmap 8812 |
. . . 4
⊢ (𝑅 ∈ (𝐵 ↑m 𝐶) ↔ 𝑅:𝐶⟶𝐵) |
23 | 21, 22 | sylibr 233 |
. . 3
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) → 𝑅 ∈ (𝐵 ↑m 𝐶)) |
24 | 17, 23 | opelxpd 5672 |
. 2
⊢ (𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) → ⟨𝐷, 𝑅⟩ ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) |
25 | | xp1st 7954 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → (1st ‘𝑦) ∈ (𝐴 ↑m 𝐶)) |
26 | 5, 8 | elmap 8812 |
. . . . . . 7
⊢
((1st ‘𝑦) ∈ (𝐴 ↑m 𝐶) ↔ (1st ‘𝑦):𝐶⟶𝐴) |
27 | 25, 26 | sylib 217 |
. . . . . 6
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → (1st ‘𝑦):𝐶⟶𝐴) |
28 | 27 | ffvelcdmda 7036 |
. . . . 5
⊢ ((𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) ∧ 𝑧 ∈ 𝐶) → ((1st ‘𝑦)‘𝑧) ∈ 𝐴) |
29 | | xp2nd 7955 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → (2nd ‘𝑦) ∈ (𝐵 ↑m 𝐶)) |
30 | 6, 8 | elmap 8812 |
. . . . . . 7
⊢
((2nd ‘𝑦) ∈ (𝐵 ↑m 𝐶) ↔ (2nd ‘𝑦):𝐶⟶𝐵) |
31 | 29, 30 | sylib 217 |
. . . . . 6
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → (2nd ‘𝑦):𝐶⟶𝐵) |
32 | 31 | ffvelcdmda 7036 |
. . . . 5
⊢ ((𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) ∧ 𝑧 ∈ 𝐶) → ((2nd ‘𝑦)‘𝑧) ∈ 𝐵) |
33 | 28, 32 | opelxpd 5672 |
. . . 4
⊢ ((𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) ∧ 𝑧 ∈ 𝐶) → ⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩ ∈ (𝐴 × 𝐵)) |
34 | | xpmapenlem.6 |
. . . 4
⊢ 𝑆 = (𝑧 ∈ 𝐶 ↦ ⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩) |
35 | 33, 34 | fmptd 7063 |
. . 3
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → 𝑆:𝐶⟶(𝐴 × 𝐵)) |
36 | 7, 8 | elmap 8812 |
. . 3
⊢ (𝑆 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ↔ 𝑆:𝐶⟶(𝐴 × 𝐵)) |
37 | 35, 36 | sylibr 233 |
. 2
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → 𝑆 ∈ ((𝐴 × 𝐵) ↑m 𝐶)) |
38 | | 1st2nd2 7961 |
. . . . 5
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩) |
39 | 38 | ad2antlr 726 |
. . . 4
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩) |
40 | 27 | feqmptd 6911 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → (1st ‘𝑦) = (𝑧 ∈ 𝐶 ↦ ((1st ‘𝑦)‘𝑧))) |
41 | 40 | ad2antlr 726 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → (1st ‘𝑦) = (𝑧 ∈ 𝐶 ↦ ((1st ‘𝑦)‘𝑧))) |
42 | | simplr 768 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → 𝑥 = 𝑆) |
43 | 42 | fveq1d 6845 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) = (𝑆‘𝑧)) |
44 | | opex 5422 |
. . . . . . . . . . . . 13
⊢
⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩ ∈ V |
45 | 34 | fvmpt2 6960 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐶 ∧ ⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩ ∈ V) → (𝑆‘𝑧) = ⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩) |
46 | 44, 45 | mpan2 690 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝐶 → (𝑆‘𝑧) = ⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩) |
47 | 46 | adantl 483 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (𝑆‘𝑧) = ⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩) |
48 | 43, 47 | eqtrd 2773 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) = ⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩) |
49 | 48 | fveq2d 6847 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (1st ‘(𝑥‘𝑧)) = (1st
‘⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩)) |
50 | | fvex 6856 |
. . . . . . . . . 10
⊢
((1st ‘𝑦)‘𝑧) ∈ V |
51 | | fvex 6856 |
. . . . . . . . . 10
⊢
((2nd ‘𝑦)‘𝑧) ∈ V |
52 | 50, 51 | op1st 7930 |
. . . . . . . . 9
⊢
(1st ‘⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩) = ((1st ‘𝑦)‘𝑧) |
53 | 49, 52 | eqtrdi 2789 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (1st ‘(𝑥‘𝑧)) = ((1st ‘𝑦)‘𝑧)) |
54 | 53 | mpteq2dva 5206 |
. . . . . . 7
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → (𝑧 ∈ 𝐶 ↦ (1st ‘(𝑥‘𝑧))) = (𝑧 ∈ 𝐶 ↦ ((1st ‘𝑦)‘𝑧))) |
55 | 14, 54 | eqtrid 2785 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → 𝐷 = (𝑧 ∈ 𝐶 ↦ ((1st ‘𝑦)‘𝑧))) |
56 | 41, 55 | eqtr4d 2776 |
. . . . 5
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → (1st ‘𝑦) = 𝐷) |
57 | 31 | feqmptd 6911 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) → (2nd ‘𝑦) = (𝑧 ∈ 𝐶 ↦ ((2nd ‘𝑦)‘𝑧))) |
58 | 57 | ad2antlr 726 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → (2nd ‘𝑦) = (𝑧 ∈ 𝐶 ↦ ((2nd ‘𝑦)‘𝑧))) |
59 | 48 | fveq2d 6847 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (2nd ‘(𝑥‘𝑧)) = (2nd
‘⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩)) |
60 | 50, 51 | op2nd 7931 |
. . . . . . . . 9
⊢
(2nd ‘⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩) = ((2nd ‘𝑦)‘𝑧) |
61 | 59, 60 | eqtrdi 2789 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) ∧ 𝑧 ∈ 𝐶) → (2nd ‘(𝑥‘𝑧)) = ((2nd ‘𝑦)‘𝑧)) |
62 | 61 | mpteq2dva 5206 |
. . . . . . 7
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → (𝑧 ∈ 𝐶 ↦ (2nd ‘(𝑥‘𝑧))) = (𝑧 ∈ 𝐶 ↦ ((2nd ‘𝑦)‘𝑧))) |
63 | 20, 62 | eqtrid 2785 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → 𝑅 = (𝑧 ∈ 𝐶 ↦ ((2nd ‘𝑦)‘𝑧))) |
64 | 58, 63 | eqtr4d 2776 |
. . . . 5
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → (2nd ‘𝑦) = 𝑅) |
65 | 56, 64 | opeq12d 4839 |
. . . 4
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ = ⟨𝐷, 𝑅⟩) |
66 | 39, 65 | eqtrd 2773 |
. . 3
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑥 = 𝑆) → 𝑦 = ⟨𝐷, 𝑅⟩) |
67 | | simpll 766 |
. . . . . 6
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶)) |
68 | 67, 9 | sylib 217 |
. . . . 5
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥:𝐶⟶(𝐴 × 𝐵)) |
69 | 68 | feqmptd 6911 |
. . . 4
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥 = (𝑧 ∈ 𝐶 ↦ (𝑥‘𝑧))) |
70 | | simpr 486 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑦 = ⟨𝐷, 𝑅⟩) |
71 | 70 | fveq2d 6847 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (1st ‘𝑦) = (1st
‘⟨𝐷, 𝑅⟩)) |
72 | 17 | ad2antrr 725 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝐷 ∈ (𝐴 ↑m 𝐶)) |
73 | 23 | ad2antrr 725 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑅 ∈ (𝐵 ↑m 𝐶)) |
74 | | op1stg 7934 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (𝐴 ↑m 𝐶) ∧ 𝑅 ∈ (𝐵 ↑m 𝐶)) → (1st ‘⟨𝐷, 𝑅⟩) = 𝐷) |
75 | 72, 73, 74 | syl2anc 585 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (1st
‘⟨𝐷, 𝑅⟩) = 𝐷) |
76 | 71, 75 | eqtrd 2773 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (1st ‘𝑦) = 𝐷) |
77 | 76 | fveq1d 6845 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → ((1st ‘𝑦)‘𝑧) = (𝐷‘𝑧)) |
78 | | fvex 6856 |
. . . . . . . . . 10
⊢
(1st ‘(𝑥‘𝑧)) ∈ V |
79 | 14 | fvmpt2 6960 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐶 ∧ (1st ‘(𝑥‘𝑧)) ∈ V) → (𝐷‘𝑧) = (1st ‘(𝑥‘𝑧))) |
80 | 78, 79 | mpan2 690 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐶 → (𝐷‘𝑧) = (1st ‘(𝑥‘𝑧))) |
81 | 77, 80 | sylan9eq 2793 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧 ∈ 𝐶) → ((1st ‘𝑦)‘𝑧) = (1st ‘(𝑥‘𝑧))) |
82 | 70 | fveq2d 6847 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (2nd ‘𝑦) = (2nd
‘⟨𝐷, 𝑅⟩)) |
83 | | op2ndg 7935 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (𝐴 ↑m 𝐶) ∧ 𝑅 ∈ (𝐵 ↑m 𝐶)) → (2nd ‘⟨𝐷, 𝑅⟩) = 𝑅) |
84 | 72, 73, 83 | syl2anc 585 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (2nd
‘⟨𝐷, 𝑅⟩) = 𝑅) |
85 | 82, 84 | eqtrd 2773 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (2nd ‘𝑦) = 𝑅) |
86 | 85 | fveq1d 6845 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → ((2nd ‘𝑦)‘𝑧) = (𝑅‘𝑧)) |
87 | | fvex 6856 |
. . . . . . . . . 10
⊢
(2nd ‘(𝑥‘𝑧)) ∈ V |
88 | 20 | fvmpt2 6960 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐶 ∧ (2nd ‘(𝑥‘𝑧)) ∈ V) → (𝑅‘𝑧) = (2nd ‘(𝑥‘𝑧))) |
89 | 87, 88 | mpan2 690 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐶 → (𝑅‘𝑧) = (2nd ‘(𝑥‘𝑧))) |
90 | 86, 89 | sylan9eq 2793 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧 ∈ 𝐶) → ((2nd ‘𝑦)‘𝑧) = (2nd ‘(𝑥‘𝑧))) |
91 | 81, 90 | opeq12d 4839 |
. . . . . . 7
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧 ∈ 𝐶) → ⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩ = ⟨(1st ‘(𝑥‘𝑧)), (2nd ‘(𝑥‘𝑧))⟩) |
92 | 68 | ffvelcdmda 7036 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) ∈ (𝐴 × 𝐵)) |
93 | | 1st2nd2 7961 |
. . . . . . . 8
⊢ ((𝑥‘𝑧) ∈ (𝐴 × 𝐵) → (𝑥‘𝑧) = ⟨(1st ‘(𝑥‘𝑧)), (2nd ‘(𝑥‘𝑧))⟩) |
94 | 92, 93 | syl 17 |
. . . . . . 7
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧 ∈ 𝐶) → (𝑥‘𝑧) = ⟨(1st ‘(𝑥‘𝑧)), (2nd ‘(𝑥‘𝑧))⟩) |
95 | 91, 94 | eqtr4d 2776 |
. . . . . 6
⊢ ((((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) ∧ 𝑧 ∈ 𝐶) → ⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩ = (𝑥‘𝑧)) |
96 | 95 | mpteq2dva 5206 |
. . . . 5
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → (𝑧 ∈ 𝐶 ↦ ⟨((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)⟩) = (𝑧 ∈ 𝐶 ↦ (𝑥‘𝑧))) |
97 | 34, 96 | eqtrid 2785 |
. . . 4
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑆 = (𝑧 ∈ 𝐶 ↦ (𝑥‘𝑧))) |
98 | 69, 97 | eqtr4d 2776 |
. . 3
⊢ (((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) ∧ 𝑦 = ⟨𝐷, 𝑅⟩) → 𝑥 = 𝑆) |
99 | 66, 98 | impbida 800 |
. 2
⊢ ((𝑥 ∈ ((𝐴 × 𝐵) ↑m 𝐶) ∧ 𝑦 ∈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶))) → (𝑥 = 𝑆 ↔ 𝑦 = ⟨𝐷, 𝑅⟩)) |
100 | 1, 4, 24, 37, 99 | en3i 8934 |
1
⊢ ((𝐴 × 𝐵) ↑m 𝐶) ≈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) |