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 16697 |
. . . 4
⊢ (𝜑 → 𝐹 = ((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))) |
6 | 5 | fveq2d 6107 |
. . 3
⊢ (𝜑 → (1st
‘𝐹) = (1st
‘((𝐷
evalF 𝐸)
∘func ((𝐺 ∘func (𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷))))) |
7 | 6 | oveqd 6566 |
. 2
⊢ (𝜑 → (𝑋(1st ‘𝐹)𝑌) = (𝑋(1st ‘((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷))))𝑌)) |
8 | | df-ov 6552 |
. . 3
⊢ (𝑋(1st ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷))))𝑌) = ((1st ‘((𝐷 evalF 𝐸) ∘func
((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷))))‘〈𝑋, 𝑌〉) |
9 | | eqid 2610 |
. . . . 5
⊢ (𝐶 ×c
𝐷) = (𝐶 ×c 𝐷) |
10 | | uncf1.a |
. . . . 5
⊢ 𝐴 = (Base‘𝐶) |
11 | | uncf1.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐷) |
12 | 9, 10, 11 | xpcbas 16641 |
. . . 4
⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷)) |
13 | | eqid 2610 |
. . . . 5
⊢ ((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)) = ((𝐺 ∘func (𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)) |
14 | | eqid 2610 |
. . . . 5
⊢ ((𝐷 FuncCat 𝐸) ×c 𝐷) = ((𝐷 FuncCat 𝐸) ×c 𝐷) |
15 | | funcrcl 16346 |
. . . . . . . . 9
⊢ (𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸)) → (𝐶 ∈ Cat ∧ (𝐷 FuncCat 𝐸) ∈ Cat)) |
16 | 4, 15 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ∈ Cat ∧ (𝐷 FuncCat 𝐸) ∈ Cat)) |
17 | 16 | simpld 474 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ Cat) |
18 | | eqid 2610 |
. . . . . . 7
⊢ (𝐶
1stF 𝐷) = (𝐶 1stF 𝐷) |
19 | 9, 17, 2, 18 | 1stfcl 16660 |
. . . . . 6
⊢ (𝜑 → (𝐶 1stF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐶)) |
20 | 19, 4 | cofucl 16371 |
. . . . 5
⊢ (𝜑 → (𝐺 ∘func (𝐶
1stF 𝐷)) ∈ ((𝐶 ×c 𝐷) Func (𝐷 FuncCat 𝐸))) |
21 | | eqid 2610 |
. . . . . 6
⊢ (𝐶
2ndF 𝐷) = (𝐶 2ndF 𝐷) |
22 | 9, 17, 2, 21 | 2ndfcl 16661 |
. . . . 5
⊢ (𝜑 → (𝐶 2ndF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐷)) |
23 | 13, 14, 20, 22 | prfcl 16666 |
. . . 4
⊢ (𝜑 → ((𝐺 ∘func (𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)) ∈ ((𝐶 ×c 𝐷) Func ((𝐷 FuncCat 𝐸) ×c 𝐷))) |
24 | | eqid 2610 |
. . . . 5
⊢ (𝐷 evalF 𝐸) = (𝐷 evalF 𝐸) |
25 | | eqid 2610 |
. . . . 5
⊢ (𝐷 FuncCat 𝐸) = (𝐷 FuncCat 𝐸) |
26 | 24, 25, 2, 3 | evlfcl 16685 |
. . . 4
⊢ (𝜑 → (𝐷 evalF 𝐸) ∈ (((𝐷 FuncCat 𝐸) ×c 𝐷) Func 𝐸)) |
27 | | uncf1.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
28 | | uncf1.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
29 | | opelxpi 5072 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐴 × 𝐵)) |
30 | 27, 28, 29 | syl2anc 691 |
. . . 4
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝐴 × 𝐵)) |
31 | 12, 23, 26, 30 | cofu1 16367 |
. . 3
⊢ (𝜑 → ((1st
‘((𝐷
evalF 𝐸)
∘func ((𝐺 ∘func (𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷))))‘〈𝑋, 𝑌〉) = ((1st ‘(𝐷 evalF 𝐸))‘((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑋, 𝑌〉))) |
32 | 8, 31 | syl5eq 2656 |
. 2
⊢ (𝜑 → (𝑋(1st ‘((𝐷 evalF 𝐸) ∘func ((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷))))𝑌) = ((1st ‘(𝐷 evalF 𝐸))‘((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑋, 𝑌〉))) |
33 | | eqid 2610 |
. . . . . . 7
⊢ (Hom
‘(𝐶
×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷)) |
34 | 13, 12, 33, 20, 22, 30 | prf1 16663 |
. . . . . 6
⊢ (𝜑 → ((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑋, 𝑌〉) = 〈((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑋, 𝑌〉), ((1st ‘(𝐶
2ndF 𝐷))‘〈𝑋, 𝑌〉)〉) |
35 | 12, 19, 4, 30 | cofu1 16367 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑋, 𝑌〉) = ((1st ‘𝐺)‘((1st
‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉))) |
36 | 9, 12, 33, 17, 2, 18, 30 | 1stf1 16655 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st
‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉) = (1st ‘〈𝑋, 𝑌〉)) |
37 | | op1stg 7071 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (1st ‘〈𝑋, 𝑌〉) = 𝑋) |
38 | 27, 28, 37 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘〈𝑋, 𝑌〉) = 𝑋) |
39 | 36, 38 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉) = 𝑋) |
40 | 39 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘𝐺)‘((1st ‘(𝐶
1stF 𝐷))‘〈𝑋, 𝑌〉)) = ((1st ‘𝐺)‘𝑋)) |
41 | 35, 40 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑋, 𝑌〉) = ((1st ‘𝐺)‘𝑋)) |
42 | 9, 12, 33, 17, 2, 21, 30 | 2ndf1 16658 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝐶
2ndF 𝐷))‘〈𝑋, 𝑌〉) = (2nd ‘〈𝑋, 𝑌〉)) |
43 | | op2ndg 7072 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (2nd ‘〈𝑋, 𝑌〉) = 𝑌) |
44 | 27, 28, 43 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘〈𝑋, 𝑌〉) = 𝑌) |
45 | 42, 44 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝐶
2ndF 𝐷))‘〈𝑋, 𝑌〉) = 𝑌) |
46 | 41, 45 | opeq12d 4348 |
. . . . . 6
⊢ (𝜑 → 〈((1st
‘(𝐺
∘func (𝐶 1stF 𝐷)))‘〈𝑋, 𝑌〉), ((1st ‘(𝐶
2ndF 𝐷))‘〈𝑋, 𝑌〉)〉 = 〈((1st
‘𝐺)‘𝑋), 𝑌〉) |
47 | 34, 46 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → ((1st
‘((𝐺
∘func (𝐶 1stF 𝐷))
〈,〉F (𝐶 2ndF 𝐷)))‘〈𝑋, 𝑌〉) = 〈((1st
‘𝐺)‘𝑋), 𝑌〉) |
48 | 47 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → ((1st
‘(𝐷
evalF 𝐸))‘((1st ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))‘〈𝑋, 𝑌〉)) = ((1st ‘(𝐷 evalF 𝐸))‘〈((1st
‘𝐺)‘𝑋), 𝑌〉)) |
49 | | df-ov 6552 |
. . . 4
⊢
(((1st ‘𝐺)‘𝑋)(1st ‘(𝐷 evalF 𝐸))𝑌) = ((1st ‘(𝐷 evalF 𝐸))‘〈((1st
‘𝐺)‘𝑋), 𝑌〉) |
50 | 48, 49 | syl6eqr 2662 |
. . 3
⊢ (𝜑 → ((1st
‘(𝐷
evalF 𝐸))‘((1st ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))‘〈𝑋, 𝑌〉)) = (((1st ‘𝐺)‘𝑋)(1st ‘(𝐷 evalF 𝐸))𝑌)) |
51 | 25 | fucbas 16443 |
. . . . . 6
⊢ (𝐷 Func 𝐸) = (Base‘(𝐷 FuncCat 𝐸)) |
52 | | relfunc 16345 |
. . . . . . 7
⊢ Rel
(𝐶 Func (𝐷 FuncCat 𝐸)) |
53 | | 1st2ndbr 7108 |
. . . . . . 7
⊢ ((Rel
(𝐶 Func (𝐷 FuncCat 𝐸)) ∧ 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) → (1st ‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
54 | 52, 4, 53 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
55 | 10, 51, 54 | funcf1 16349 |
. . . . 5
⊢ (𝜑 → (1st
‘𝐺):𝐴⟶(𝐷 Func 𝐸)) |
56 | 55, 27 | ffvelrnd 6268 |
. . . 4
⊢ (𝜑 → ((1st
‘𝐺)‘𝑋) ∈ (𝐷 Func 𝐸)) |
57 | 24, 2, 3, 11, 56, 28 | evlf1 16683 |
. . 3
⊢ (𝜑 → (((1st
‘𝐺)‘𝑋)(1st ‘(𝐷 evalF 𝐸))𝑌) = ((1st ‘((1st
‘𝐺)‘𝑋))‘𝑌)) |
58 | 50, 57 | eqtrd 2644 |
. 2
⊢ (𝜑 → ((1st
‘(𝐷
evalF 𝐸))‘((1st ‘((𝐺 ∘func
(𝐶
1stF 𝐷)) 〈,〉F (𝐶
2ndF 𝐷)))‘〈𝑋, 𝑌〉)) = ((1st
‘((1st ‘𝐺)‘𝑋))‘𝑌)) |
59 | 7, 32, 58 | 3eqtrd 2648 |
1
⊢ (𝜑 → (𝑋(1st ‘𝐹)𝑌) = ((1st ‘((1st
‘𝐺)‘𝑋))‘𝑌)) |