Description: Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 15-Jul-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cofmpt2.1 | |
|
cofmpt2.2 | |
||
cofmpt2.3 | |
||
cofmpt2.4 | |
||
Assertion | cofmpt2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cofmpt2.1 | |
|
2 | cofmpt2.2 | |
|
3 | cofmpt2.3 | |
|
4 | cofmpt2.4 | |
|
5 | 2 | fmpttd | |
6 | fcompt | |
|
7 | 5 3 6 | syl2anc | |
8 | eqid | |
|
9 | 1 | adantlr | |
10 | 3 | ffvelrnda | |
11 | 4 | adantr | |
12 | 8 9 10 11 | fvmptd2 | |
13 | 12 | mpteq2dva | |
14 | 7 13 | eqtrd | |