Detailed syntax breakdown of Definition df-evlf
Step | Hyp | Ref
| Expression |
1 | | cevlf 17717 |
. 2
class
evalF |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | vd |
. . 3
setvar 𝑑 |
4 | | ccat 17167 |
. . 3
class
Cat |
5 | | vf |
. . . . 5
setvar 𝑓 |
6 | | vx |
. . . . 5
setvar 𝑥 |
7 | 2 | cv 1542 |
. . . . . 6
class 𝑐 |
8 | 3 | cv 1542 |
. . . . . 6
class 𝑑 |
9 | | cfunc 17360 |
. . . . . 6
class
Func |
10 | 7, 8, 9 | co 7213 |
. . . . 5
class (𝑐 Func 𝑑) |
11 | | cbs 16760 |
. . . . . 6
class
Base |
12 | 7, 11 | cfv 6380 |
. . . . 5
class
(Base‘𝑐) |
13 | 6 | cv 1542 |
. . . . . 6
class 𝑥 |
14 | 5 | cv 1542 |
. . . . . . 7
class 𝑓 |
15 | | c1st 7759 |
. . . . . . 7
class
1st |
16 | 14, 15 | cfv 6380 |
. . . . . 6
class
(1st ‘𝑓) |
17 | 13, 16 | cfv 6380 |
. . . . 5
class
((1st ‘𝑓)‘𝑥) |
18 | 5, 6, 10, 12, 17 | cmpo 7215 |
. . . 4
class (𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1st ‘𝑓)‘𝑥)) |
19 | | vy |
. . . . 5
setvar 𝑦 |
20 | 10, 12 | cxp 5549 |
. . . . 5
class ((𝑐 Func 𝑑) × (Base‘𝑐)) |
21 | | vm |
. . . . . 6
setvar 𝑚 |
22 | 13, 15 | cfv 6380 |
. . . . . 6
class
(1st ‘𝑥) |
23 | | vn |
. . . . . . 7
setvar 𝑛 |
24 | 19 | cv 1542 |
. . . . . . . 8
class 𝑦 |
25 | 24, 15 | cfv 6380 |
. . . . . . 7
class
(1st ‘𝑦) |
26 | | va |
. . . . . . . 8
setvar 𝑎 |
27 | | vg |
. . . . . . . 8
setvar 𝑔 |
28 | 21 | cv 1542 |
. . . . . . . . 9
class 𝑚 |
29 | 23 | cv 1542 |
. . . . . . . . 9
class 𝑛 |
30 | | cnat 17448 |
. . . . . . . . . 10
class
Nat |
31 | 7, 8, 30 | co 7213 |
. . . . . . . . 9
class (𝑐 Nat 𝑑) |
32 | 28, 29, 31 | co 7213 |
. . . . . . . 8
class (𝑚(𝑐 Nat 𝑑)𝑛) |
33 | | c2nd 7760 |
. . . . . . . . . 10
class
2nd |
34 | 13, 33 | cfv 6380 |
. . . . . . . . 9
class
(2nd ‘𝑥) |
35 | 24, 33 | cfv 6380 |
. . . . . . . . 9
class
(2nd ‘𝑦) |
36 | | chom 16813 |
. . . . . . . . . 10
class
Hom |
37 | 7, 36 | cfv 6380 |
. . . . . . . . 9
class (Hom
‘𝑐) |
38 | 34, 35, 37 | co 7213 |
. . . . . . . 8
class
((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) |
39 | 26 | cv 1542 |
. . . . . . . . . 10
class 𝑎 |
40 | 35, 39 | cfv 6380 |
. . . . . . . . 9
class (𝑎‘(2nd
‘𝑦)) |
41 | 27 | cv 1542 |
. . . . . . . . . 10
class 𝑔 |
42 | 28, 33 | cfv 6380 |
. . . . . . . . . . 11
class
(2nd ‘𝑚) |
43 | 34, 35, 42 | co 7213 |
. . . . . . . . . 10
class
((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦)) |
44 | 41, 43 | cfv 6380 |
. . . . . . . . 9
class
(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔) |
45 | 28, 15 | cfv 6380 |
. . . . . . . . . . . 12
class
(1st ‘𝑚) |
46 | 34, 45 | cfv 6380 |
. . . . . . . . . . 11
class
((1st ‘𝑚)‘(2nd ‘𝑥)) |
47 | 35, 45 | cfv 6380 |
. . . . . . . . . . 11
class
((1st ‘𝑚)‘(2nd ‘𝑦)) |
48 | 46, 47 | cop 4547 |
. . . . . . . . . 10
class
〈((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 |
49 | 29, 15 | cfv 6380 |
. . . . . . . . . . 11
class
(1st ‘𝑛) |
50 | 35, 49 | cfv 6380 |
. . . . . . . . . 10
class
((1st ‘𝑛)‘(2nd ‘𝑦)) |
51 | | cco 16814 |
. . . . . . . . . . 11
class
comp |
52 | 8, 51 | cfv 6380 |
. . . . . . . . . 10
class
(comp‘𝑑) |
53 | 48, 50, 52 | co 7213 |
. . . . . . . . 9
class
(〈((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝑑)((1st ‘𝑛)‘(2nd
‘𝑦))) |
54 | 40, 44, 53 | co 7213 |
. . . . . . . 8
class ((𝑎‘(2nd
‘𝑦))(〈((1st ‘𝑚)‘(2nd
‘𝑥)),
((1st ‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝑑)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)) |
55 | 26, 27, 32, 38, 54 | cmpo 7215 |
. . . . . . 7
class (𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝑑)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) |
56 | 23, 25, 55 | csb 3811 |
. . . . . 6
class
⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝑑)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) |
57 | 21, 22, 56 | csb 3811 |
. . . . 5
class
⦋(1st ‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝑑)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) |
58 | 6, 19, 20, 20, 57 | cmpo 7215 |
. . . 4
class (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝑑)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) |
59 | 18, 58 | cop 4547 |
. . 3
class
〈(𝑓 ∈
(𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝑑)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))〉 |
60 | 2, 3, 4, 4, 59 | cmpo 7215 |
. 2
class (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ 〈(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝑑)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))〉) |
61 | 1, 60 | wceq 1543 |
1
wff
evalF = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ 〈(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝑑)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))〉) |