Step | Hyp | Ref
| Expression |
1 | | cevlf 17453 |
. 2
class
eval_{F} |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | vd |
. . 3
setvar 𝑑 |
4 | | ccat 16929 |
. . 3
class
Cat |
5 | | vf |
. . . . 5
setvar 𝑓 |
6 | | vx |
. . . . 5
setvar 𝑥 |
7 | 2 | cv 1537 |
. . . . . 6
class 𝑐 |
8 | 3 | cv 1537 |
. . . . . 6
class 𝑑 |
9 | | cfunc 17118 |
. . . . . 6
class
Func |
10 | 7, 8, 9 | co 7135 |
. . . . 5
class (𝑐 Func 𝑑) |
11 | | cbs 16477 |
. . . . . 6
class
Base |
12 | 7, 11 | cfv 6324 |
. . . . 5
class
(Base‘𝑐) |
13 | 6 | cv 1537 |
. . . . . 6
class 𝑥 |
14 | 5 | cv 1537 |
. . . . . . 7
class 𝑓 |
15 | | c1st 7671 |
. . . . . . 7
class
1^{st} |
16 | 14, 15 | cfv 6324 |
. . . . . 6
class
(1^{st} ‘𝑓) |
17 | 13, 16 | cfv 6324 |
. . . . 5
class
((1^{st} ‘𝑓)‘𝑥) |
18 | 5, 6, 10, 12, 17 | cmpo 7137 |
. . . 4
class (𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1^{st} ‘𝑓)‘𝑥)) |
19 | | vy |
. . . . 5
setvar 𝑦 |
20 | 10, 12 | cxp 5517 |
. . . . 5
class ((𝑐 Func 𝑑) × (Base‘𝑐)) |
21 | | vm |
. . . . . 6
setvar 𝑚 |
22 | 13, 15 | cfv 6324 |
. . . . . 6
class
(1^{st} ‘𝑥) |
23 | | vn |
. . . . . . 7
setvar 𝑛 |
24 | 19 | cv 1537 |
. . . . . . . 8
class 𝑦 |
25 | 24, 15 | cfv 6324 |
. . . . . . 7
class
(1^{st} ‘𝑦) |
26 | | va |
. . . . . . . 8
setvar 𝑎 |
27 | | vg |
. . . . . . . 8
setvar 𝑔 |
28 | 21 | cv 1537 |
. . . . . . . . 9
class 𝑚 |
29 | 23 | cv 1537 |
. . . . . . . . 9
class 𝑛 |
30 | | cnat 17205 |
. . . . . . . . . 10
class
Nat |
31 | 7, 8, 30 | co 7135 |
. . . . . . . . 9
class (𝑐 Nat 𝑑) |
32 | 28, 29, 31 | co 7135 |
. . . . . . . 8
class (𝑚(𝑐 Nat 𝑑)𝑛) |
33 | | c2nd 7672 |
. . . . . . . . . 10
class
2^{nd} |
34 | 13, 33 | cfv 6324 |
. . . . . . . . 9
class
(2^{nd} ‘𝑥) |
35 | 24, 33 | cfv 6324 |
. . . . . . . . 9
class
(2^{nd} ‘𝑦) |
36 | | chom 16570 |
. . . . . . . . . 10
class
Hom |
37 | 7, 36 | cfv 6324 |
. . . . . . . . 9
class (Hom
‘𝑐) |
38 | 34, 35, 37 | co 7135 |
. . . . . . . 8
class
((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) |
39 | 26 | cv 1537 |
. . . . . . . . . 10
class 𝑎 |
40 | 35, 39 | cfv 6324 |
. . . . . . . . 9
class (𝑎‘(2^{nd}
‘𝑦)) |
41 | 27 | cv 1537 |
. . . . . . . . . 10
class 𝑔 |
42 | 28, 33 | cfv 6324 |
. . . . . . . . . . 11
class
(2^{nd} ‘𝑚) |
43 | 34, 35, 42 | co 7135 |
. . . . . . . . . 10
class
((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦)) |
44 | 41, 43 | cfv 6324 |
. . . . . . . . 9
class
(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔) |
45 | 28, 15 | cfv 6324 |
. . . . . . . . . . . 12
class
(1^{st} ‘𝑚) |
46 | 34, 45 | cfv 6324 |
. . . . . . . . . . 11
class
((1^{st} ‘𝑚)‘(2^{nd} ‘𝑥)) |
47 | 35, 45 | cfv 6324 |
. . . . . . . . . . 11
class
((1^{st} ‘𝑚)‘(2^{nd} ‘𝑦)) |
48 | 46, 47 | cop 4531 |
. . . . . . . . . 10
class
⟨((1^{st} ‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩ |
49 | 29, 15 | cfv 6324 |
. . . . . . . . . . 11
class
(1^{st} ‘𝑛) |
50 | 35, 49 | cfv 6324 |
. . . . . . . . . 10
class
((1^{st} ‘𝑛)‘(2^{nd} ‘𝑦)) |
51 | | cco 16571 |
. . . . . . . . . . 11
class
comp |
52 | 8, 51 | cfv 6324 |
. . . . . . . . . 10
class
(comp‘𝑑) |
53 | 48, 50, 52 | co 7135 |
. . . . . . . . 9
class
(⟨((1^{st} ‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦))) |
54 | 40, 44, 53 | co 7135 |
. . . . . . . 8
class ((𝑎‘(2^{nd}
‘𝑦))(⟨((1^{st} ‘𝑚)‘(2^{nd}
‘𝑥)),
((1^{st} ‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔)) |
55 | 26, 27, 32, 38, 54 | cmpo 7137 |
. . . . . . 7
class (𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔))) |
56 | 23, 25, 55 | csb 3828 |
. . . . . 6
class
⦋(1^{st} ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔))) |
57 | 21, 22, 56 | csb 3828 |
. . . . 5
class
⦋(1^{st} ‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔))) |
58 | 6, 19, 20, 20, 57 | cmpo 7137 |
. . . 4
class (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔)))) |
59 | 18, 58 | cop 4531 |
. . 3
class
⟨(𝑓 ∈
(𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1^{st} ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔))))⟩ |
60 | 2, 3, 4, 4, 59 | cmpo 7137 |
. 2
class (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ ⟨(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1^{st} ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔))))⟩) |
61 | 1, 60 | wceq 1538 |
1
wff
eval_{F} = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ ⟨(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1^{st} ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔))))⟩) |