Description: Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | comfffval2.o | |
|
comfffval2.b | |
||
comfffval2.h | |
||
comfffval2.x | |
||
Assertion | comfffval2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | comfffval2.o | |
|
2 | comfffval2.b | |
|
3 | comfffval2.h | |
|
4 | comfffval2.x | |
|
5 | eqid | |
|
6 | 1 2 5 4 | comfffval | |
7 | xp2nd | |
|
8 | 7 | adantr | |
9 | simpr | |
|
10 | 3 2 5 8 9 | homfval | |
11 | xp1st | |
|
12 | 11 | adantr | |
13 | 3 2 5 12 8 | homfval | |
14 | df-ov | |
|
15 | df-ov | |
|
16 | 13 14 15 | 3eqtr3g | |
17 | 1st2nd2 | |
|
18 | 17 | adantr | |
19 | 18 | fveq2d | |
20 | 18 | fveq2d | |
21 | 16 19 20 | 3eqtr4d | |
22 | eqidd | |
|
23 | 10 21 22 | mpoeq123dv | |
24 | 23 | mpoeq3ia | |
25 | 6 24 | eqtr4i | |