Proof of Theorem uncf1
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 17742 |
. . . 4
⊢ (𝜑 → 𝐹 = ((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))) |
6 | 5 | fveq2d 6721 |
. . 3
⊢ (𝜑 → (1st
‘𝐹) = (1st
‘((𝐷
evalF 𝐸)
∘func ((𝐺 ∘func (𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷))))) |
7 | 6 | oveqd 7230 |
. 2
⊢ (𝜑 → (𝑋(1st ‘𝐹)𝑌) = (𝑋(1st ‘((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷))))𝑌)) |
8 | | df-ov 7216 |
. . 3
⊢ (𝑋(1st ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷))))𝑌) = ((1st ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷))))‘〈𝑋, 𝑌〉) |
9 | | eqid 2737 |
. . . . 5
⊢ (𝐶 ×c
𝐷) = (𝐶 ×c 𝐷) |
10 | | uncf1.a |
. . . . 5
⊢ 𝐴 = (Base‘𝐶) |
11 | | uncf1.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐷) |
12 | 9, 10, 11 | xpcbas 17685 |
. . . 4
⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷)) |
13 | | eqid 2737 |
. . . . 5
⊢ ((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)) = ((𝐺 ∘func (𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)) |
14 | | eqid 2737 |
. . . . 5
⊢ ((𝐷 FuncCat 𝐸) ×c 𝐷) = ((𝐷 FuncCat 𝐸) ×c 𝐷) |
15 | | funcrcl 17369 |
. . . . . . . . 9
⊢ (𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸)) → (𝐶 ∈ Cat ∧ (𝐷 FuncCat 𝐸) ∈ Cat)) |
16 | 4, 15 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ∈ Cat ∧ (𝐷 FuncCat 𝐸) ∈ Cat)) |
17 | 16 | simpld 498 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ Cat) |
18 | | eqid 2737 |
. . . . . . 7
⊢ (𝐶
1stF 𝐷) = (𝐶 1stF 𝐷) |
19 | 9, 17, 2, 18 | 1stfcl 17704 |
. . . . . 6
⊢ (𝜑 → (𝐶 1stF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐶)) |
20 | 19, 4 | cofucl 17394 |
. . . . 5
⊢ (𝜑 → (𝐺 ∘func (𝐶
1stF 𝐷)) ∈ ((𝐶 ×c 𝐷) Func (𝐷 FuncCat 𝐸))) |
21 | | eqid 2737 |
. . . . . 6
⊢ (𝐶
2ndF 𝐷) = (𝐶 2ndF 𝐷) |
22 | 9, 17, 2, 21 | 2ndfcl 17705 |
. . . . 5
⊢ (𝜑 → (𝐶 2ndF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐷)) |
23 | 13, 14, 20, 22 | prfcl 17710 |
. . . 4
⊢ (𝜑 → ((𝐺 ∘func (𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)) ∈ ((𝐶 ×c 𝐷) Func ((𝐷 FuncCat 𝐸) ×c 𝐷))) |
24 | | eqid 2737 |
. . . . 5
⊢ (𝐷 evalF 𝐸) = (𝐷 evalF 𝐸) |
25 | | eqid 2737 |
. . . . 5
⊢ (𝐷 FuncCat 𝐸) = (𝐷 FuncCat 𝐸) |
26 | 24, 25, 2, 3 | evlfcl 17730 |
. . . 4
⊢ (𝜑 → (𝐷 evalF 𝐸) ∈ (((𝐷 FuncCat 𝐸) ×c 𝐷) Func 𝐸)) |
27 | | uncf1.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
28 | | uncf1.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
29 | 27, 28 | opelxpd 5589 |
. . . 4
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝐴 × 𝐵)) |
30 | 12, 23, 26, 29 | cofu1 17390 |
. . 3
⊢ (𝜑 → ((1st
‘((𝐷
evalF 𝐸)
∘func ((𝐺 ∘func (𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷))))‘〈𝑋, 𝑌〉) = ((1st ‘(𝐷 evalF 𝐸))‘((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑋, 𝑌〉))) |
31 | 8, 30 | syl5eq 2790 |
. 2
⊢ (𝜑 → (𝑋(1st ‘((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷))))𝑌) = ((1st ‘(𝐷 evalF 𝐸))‘((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑋, 𝑌〉))) |
32 | | eqid 2737 |
. . . . . . 7
⊢ (Hom
‘(𝐶
×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷)) |
33 | 13, 12, 32, 20, 22, 29 | prf1 17707 |
. . . . . 6
⊢ (𝜑 → ((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑋, 𝑌〉) = 〈((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑋, 𝑌〉), ((1st ‘(𝐶
2ndF 𝐷))‘〈𝑋, 𝑌〉)〉) |
34 | 12, 19, 4, 29 | cofu1 17390 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑋, 𝑌〉) = ((1st ‘𝐺)‘((1st
‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉))) |
35 | 9, 12, 32, 17, 2, 18, 29 | 1stf1 17699 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st
‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉) = (1st ‘〈𝑋, 𝑌〉)) |
36 | | op1stg 7773 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (1st ‘〈𝑋, 𝑌〉) = 𝑋) |
37 | 27, 28, 36 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘〈𝑋, 𝑌〉) = 𝑋) |
38 | 35, 37 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉) = 𝑋) |
39 | 38 | fveq2d 6721 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘𝐺)‘((1st ‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉)) = ((1st ‘𝐺)‘𝑋)) |
40 | 34, 39 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑋, 𝑌〉) = ((1st ‘𝐺)‘𝑋)) |
41 | 9, 12, 32, 17, 2, 21, 29 | 2ndf1 17702 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝐶
2ndF 𝐷))‘〈𝑋, 𝑌〉) = (2nd ‘〈𝑋, 𝑌〉)) |
42 | | op2ndg 7774 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (2nd ‘〈𝑋, 𝑌〉) = 𝑌) |
43 | 27, 28, 42 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘〈𝑋, 𝑌〉) = 𝑌) |
44 | 41, 43 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝐶
2ndF 𝐷))‘〈𝑋, 𝑌〉) = 𝑌) |
45 | 40, 44 | opeq12d 4792 |
. . . . . 6
⊢ (𝜑 → 〈((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑋, 𝑌〉), ((1st ‘(𝐶
2ndF 𝐷))‘〈𝑋, 𝑌〉)〉 = 〈((1st
‘𝐺)‘𝑋), 𝑌〉) |
46 | 33, 45 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → ((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑋, 𝑌〉) = 〈((1st
‘𝐺)‘𝑋), 𝑌〉) |
47 | 46 | fveq2d 6721 |
. . . 4
⊢ (𝜑 → ((1st
‘(𝐷
evalF 𝐸))‘((1st ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))‘〈𝑋, 𝑌〉)) = ((1st ‘(𝐷 evalF 𝐸))‘〈((1st
‘𝐺)‘𝑋), 𝑌〉)) |
48 | | df-ov 7216 |
. . . 4
⊢
(((1st ‘𝐺)‘𝑋)(1st ‘(𝐷 evalF 𝐸))𝑌) = ((1st ‘(𝐷 evalF 𝐸))‘〈((1st
‘𝐺)‘𝑋), 𝑌〉) |
49 | 47, 48 | eqtr4di 2796 |
. . 3
⊢ (𝜑 → ((1st
‘(𝐷
evalF 𝐸))‘((1st ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))‘〈𝑋, 𝑌〉)) = (((1st ‘𝐺)‘𝑋)(1st ‘(𝐷 evalF 𝐸))𝑌)) |
50 | 25 | fucbas 17468 |
. . . . . 6
⊢ (𝐷 Func 𝐸) = (Base‘(𝐷 FuncCat 𝐸)) |
51 | | relfunc 17368 |
. . . . . . 7
⊢ Rel
(𝐶 Func (𝐷 FuncCat 𝐸)) |
52 | | 1st2ndbr 7813 |
. . . . . . 7
⊢ ((Rel
(𝐶 Func (𝐷 FuncCat 𝐸)) ∧ 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) → (1st ‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
53 | 51, 4, 52 | sylancr 590 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
54 | 10, 50, 53 | funcf1 17372 |
. . . . 5
⊢ (𝜑 → (1st
‘𝐺):𝐴⟶(𝐷 Func 𝐸)) |
55 | 54, 27 | ffvelrnd 6905 |
. . . 4
⊢ (𝜑 → ((1st
‘𝐺)‘𝑋) ∈ (𝐷 Func 𝐸)) |
56 | 24, 2, 3, 11, 55, 28 | evlf1 17728 |
. . 3
⊢ (𝜑 → (((1st
‘𝐺)‘𝑋)(1st ‘(𝐷 evalF 𝐸))𝑌) = ((1st ‘((1st
‘𝐺)‘𝑋))‘𝑌)) |
57 | 49, 56 | eqtrd 2777 |
. 2
⊢ (𝜑 → ((1st
‘(𝐷
evalF 𝐸))‘((1st ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))‘〈𝑋, 𝑌〉)) = ((1st
‘((1st ‘𝐺)‘𝑋))‘𝑌)) |
58 | 7, 31, 57 | 3eqtrd 2781 |
1
⊢ (𝜑 → (𝑋(1st ‘𝐹)𝑌) = ((1st ‘((1st
‘𝐺)‘𝑋))‘𝑌)) |