Description: Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017) (Proof shortened by AV, 1-Mar-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | natfval.1 | |
|
natfval.b | |
||
natfval.h | |
||
natfval.j | |
||
natfval.o | |
||
Assertion | natfval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | natfval.1 | |
|
2 | natfval.b | |
|
3 | natfval.h | |
|
4 | natfval.j | |
|
5 | natfval.o | |
|
6 | oveq12 | |
|
7 | simpl | |
|
8 | 7 | fveq2d | |
9 | 8 2 | eqtr4di | |
10 | 9 | ixpeq1d | |
11 | simpr | |
|
12 | 11 | fveq2d | |
13 | 12 4 | eqtr4di | |
14 | 13 | oveqd | |
15 | 14 | ixpeq2dv | |
16 | 10 15 | eqtrd | |
17 | 7 | fveq2d | |
18 | 17 3 | eqtr4di | |
19 | 18 | oveqd | |
20 | 11 | fveq2d | |
21 | 20 5 | eqtr4di | |
22 | 21 | oveqd | |
23 | 22 | oveqd | |
24 | 21 | oveqd | |
25 | 24 | oveqd | |
26 | 23 25 | eqeq12d | |
27 | 19 26 | raleqbidv | |
28 | 9 27 | raleqbidv | |
29 | 9 28 | raleqbidv | |
30 | 16 29 | rabeqbidv | |
31 | 30 | csbeq2dv | |
32 | 31 | csbeq2dv | |
33 | 6 6 32 | mpoeq123dv | |
34 | df-nat | |
|
35 | ovex | |
|
36 | 35 35 | mpoex | |
37 | 33 34 36 | ovmpoa | |
38 | 34 | mpondm0 | |
39 | funcrcl | |
|
40 | 39 | con3i | |
41 | 40 | eq0rdv | |
42 | 41 | olcd | |
43 | 0mpo0 | |
|
44 | 42 43 | syl | |
45 | 38 44 | eqtr4d | |
46 | 37 45 | pm2.61i | |
47 | 1 46 | eqtri | |