Step | Hyp | Ref
| Expression |
1 | | uncfval.g |
. . . . 5
⊢ 𝐹 = (⟨“𝐶𝐷𝐸”⟩ uncurryF
𝐺) |
2 | | uncfval.c |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ Cat) |
3 | | uncfval.d |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ Cat) |
4 | | uncfval.f |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) |
5 | 1, 2, 3, 4 | uncfval 18128 |
. . . 4
⊢ (𝜑 → 𝐹 = ((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))) |
6 | 5 | fveq2d 6847 |
. . 3
⊢ (𝜑 → (1st
‘𝐹) = (1st
‘((𝐷
evalF 𝐸)
∘func ((𝐺 ∘func (𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷))))) |
7 | 6 | oveqd 7375 |
. 2
⊢ (𝜑 → (𝑋(1st ‘𝐹)𝑌) = (𝑋(1st ‘((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷))))𝑌)) |
8 | | df-ov 7361 |
. . 3
⊢ (𝑋(1st ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷))))𝑌) = ((1st ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷))))‘⟨𝑋, 𝑌⟩) |
9 | | eqid 2733 |
. . . . 5
⊢ (𝐶 ×c
𝐷) = (𝐶 ×c 𝐷) |
10 | | uncf1.a |
. . . . 5
⊢ 𝐴 = (Base‘𝐶) |
11 | | uncf1.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐷) |
12 | 9, 10, 11 | xpcbas 18071 |
. . . 4
⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷)) |
13 | | eqid 2733 |
. . . . 5
⊢ ((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)) = ((𝐺 ∘func (𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)) |
14 | | eqid 2733 |
. . . . 5
⊢ ((𝐷 FuncCat 𝐸) ×c 𝐷) = ((𝐷 FuncCat 𝐸) ×c 𝐷) |
15 | | funcrcl 17754 |
. . . . . . . . 9
⊢ (𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸)) → (𝐶 ∈ Cat ∧ (𝐷 FuncCat 𝐸) ∈ Cat)) |
16 | 4, 15 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ∈ Cat ∧ (𝐷 FuncCat 𝐸) ∈ Cat)) |
17 | 16 | simpld 496 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ Cat) |
18 | | eqid 2733 |
. . . . . . 7
⊢ (𝐶
1stF 𝐷) = (𝐶 1stF 𝐷) |
19 | 9, 17, 2, 18 | 1stfcl 18090 |
. . . . . 6
⊢ (𝜑 → (𝐶 1stF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐶)) |
20 | 19, 4 | cofucl 17779 |
. . . . 5
⊢ (𝜑 → (𝐺 ∘func (𝐶
1stF 𝐷)) ∈ ((𝐶 ×c 𝐷) Func (𝐷 FuncCat 𝐸))) |
21 | | eqid 2733 |
. . . . . 6
⊢ (𝐶
2ndF 𝐷) = (𝐶 2ndF 𝐷) |
22 | 9, 17, 2, 21 | 2ndfcl 18091 |
. . . . 5
⊢ (𝜑 → (𝐶 2ndF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐷)) |
23 | 13, 14, 20, 22 | prfcl 18096 |
. . . 4
⊢ (𝜑 → ((𝐺 ∘func (𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)) ∈ ((𝐶 ×c 𝐷) Func ((𝐷 FuncCat 𝐸) ×c 𝐷))) |
24 | | eqid 2733 |
. . . . 5
⊢ (𝐷 evalF 𝐸) = (𝐷 evalF 𝐸) |
25 | | eqid 2733 |
. . . . 5
⊢ (𝐷 FuncCat 𝐸) = (𝐷 FuncCat 𝐸) |
26 | 24, 25, 2, 3 | evlfcl 18116 |
. . . 4
⊢ (𝜑 → (𝐷 evalF 𝐸) ∈ (((𝐷 FuncCat 𝐸) ×c 𝐷) Func 𝐸)) |
27 | | uncf1.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
28 | | uncf1.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
29 | 27, 28 | opelxpd 5672 |
. . . 4
⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝐴 × 𝐵)) |
30 | 12, 23, 26, 29 | cofu1 17775 |
. . 3
⊢ (𝜑 → ((1st
‘((𝐷
evalF 𝐸)
∘func ((𝐺 ∘func (𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷))))‘⟨𝑋, 𝑌⟩) = ((1st ‘(𝐷 evalF 𝐸))‘((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑋, 𝑌⟩))) |
31 | 8, 30 | eqtrid 2785 |
. 2
⊢ (𝜑 → (𝑋(1st ‘((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷))))𝑌) = ((1st ‘(𝐷 evalF 𝐸))‘((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑋, 𝑌⟩))) |
32 | | eqid 2733 |
. . . . . . 7
⊢ (Hom
‘(𝐶
×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷)) |
33 | 13, 12, 32, 20, 22, 29 | prf1 18093 |
. . . . . 6
⊢ (𝜑 → ((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑋, 𝑌⟩) = ⟨((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘⟨𝑋, 𝑌⟩), ((1st ‘(𝐶
2ndF 𝐷))‘⟨𝑋, 𝑌⟩)⟩) |
34 | 12, 19, 4, 29 | cofu1 17775 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘⟨𝑋, 𝑌⟩) = ((1st ‘𝐺)‘((1st
‘(𝐶
1stF 𝐷))‘⟨𝑋, 𝑌⟩))) |
35 | 9, 12, 32, 17, 2, 18, 29 | 1stf1 18085 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st
‘(𝐶
1stF 𝐷))‘⟨𝑋, 𝑌⟩) = (1st ‘⟨𝑋, 𝑌⟩)) |
36 | | op1stg 7934 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋) |
37 | 27, 28, 36 | syl2anc 585 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘⟨𝑋, 𝑌⟩) = 𝑋) |
38 | 35, 37 | eqtrd 2773 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(𝐶
1stF 𝐷))‘⟨𝑋, 𝑌⟩) = 𝑋) |
39 | 38 | fveq2d 6847 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘𝐺)‘((1st ‘(𝐶
1stF 𝐷))‘⟨𝑋, 𝑌⟩)) = ((1st ‘𝐺)‘𝑋)) |
40 | 34, 39 | eqtrd 2773 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘⟨𝑋, 𝑌⟩) = ((1st ‘𝐺)‘𝑋)) |
41 | 9, 12, 32, 17, 2, 21, 29 | 2ndf1 18088 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝐶
2ndF 𝐷))‘⟨𝑋, 𝑌⟩) = (2nd ‘⟨𝑋, 𝑌⟩)) |
42 | | op2ndg 7935 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌) |
43 | 27, 28, 42 | syl2anc 585 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘⟨𝑋, 𝑌⟩) = 𝑌) |
44 | 41, 43 | eqtrd 2773 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝐶
2ndF 𝐷))‘⟨𝑋, 𝑌⟩) = 𝑌) |
45 | 40, 44 | opeq12d 4839 |
. . . . . 6
⊢ (𝜑 → ⟨((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘⟨𝑋, 𝑌⟩), ((1st ‘(𝐶
2ndF 𝐷))‘⟨𝑋, 𝑌⟩)⟩ = ⟨((1st
‘𝐺)‘𝑋), 𝑌⟩) |
46 | 33, 45 | eqtrd 2773 |
. . . . 5
⊢ (𝜑 → ((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
⟨,⟩F (𝐶 2ndF 𝐷)))‘⟨𝑋, 𝑌⟩) = ⟨((1st
‘𝐺)‘𝑋), 𝑌⟩) |
47 | 46 | fveq2d 6847 |
. . . 4
⊢ (𝜑 → ((1st
‘(𝐷
evalF 𝐸))‘((1st ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))‘⟨𝑋, 𝑌⟩)) = ((1st ‘(𝐷 evalF 𝐸))‘⟨((1st
‘𝐺)‘𝑋), 𝑌⟩)) |
48 | | df-ov 7361 |
. . . 4
⊢
(((1st ‘𝐺)‘𝑋)(1st ‘(𝐷 evalF 𝐸))𝑌) = ((1st ‘(𝐷 evalF 𝐸))‘⟨((1st
‘𝐺)‘𝑋), 𝑌⟩) |
49 | 47, 48 | eqtr4di 2791 |
. . 3
⊢ (𝜑 → ((1st
‘(𝐷
evalF 𝐸))‘((1st ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))‘⟨𝑋, 𝑌⟩)) = (((1st ‘𝐺)‘𝑋)(1st ‘(𝐷 evalF 𝐸))𝑌)) |
50 | 25 | fucbas 17853 |
. . . . . 6
⊢ (𝐷 Func 𝐸) = (Base‘(𝐷 FuncCat 𝐸)) |
51 | | relfunc 17753 |
. . . . . . 7
⊢ Rel
(𝐶 Func (𝐷 FuncCat 𝐸)) |
52 | | 1st2ndbr 7975 |
. . . . . . 7
⊢ ((Rel
(𝐶 Func (𝐷 FuncCat 𝐸)) ∧ 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) → (1st ‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
53 | 51, 4, 52 | sylancr 588 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
54 | 10, 50, 53 | funcf1 17757 |
. . . . 5
⊢ (𝜑 → (1st
‘𝐺):𝐴⟶(𝐷 Func 𝐸)) |
55 | 54, 27 | ffvelcdmd 7037 |
. . . 4
⊢ (𝜑 → ((1st
‘𝐺)‘𝑋) ∈ (𝐷 Func 𝐸)) |
56 | 24, 2, 3, 11, 55, 28 | evlf1 18114 |
. . 3
⊢ (𝜑 → (((1st
‘𝐺)‘𝑋)(1st ‘(𝐷 evalF 𝐸))𝑌) = ((1st ‘((1st
‘𝐺)‘𝑋))‘𝑌)) |
57 | 49, 56 | eqtrd 2773 |
. 2
⊢ (𝜑 → ((1st
‘(𝐷
evalF 𝐸))‘((1st ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) ⟨,⟩F (𝐶
2ndF 𝐷)))‘⟨𝑋, 𝑌⟩)) = ((1st
‘((1st ‘𝐺)‘𝑋))‘𝑌)) |
58 | 7, 31, 57 | 3eqtrd 2777 |
1
⊢ (𝜑 → (𝑋(1st ‘𝐹)𝑌) = ((1st ‘((1st
‘𝐺)‘𝑋))‘𝑌)) |