Description: The value of a unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 1arympt1.f | |
|
Assertion | 1arympt1fv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1arympt1.f | |
|
2 | 1 | a1i | |
3 | fveq1 | |
|
4 | 3 | adantl | |
5 | c0ex | |
|
6 | 5 | a1i | |
7 | 6 | anim1i | |
8 | 7 | adantr | |
9 | fvsng | |
|
10 | 8 9 | syl | |
11 | 4 10 | eqtrd | |
12 | 11 | fveq2d | |
13 | 5 | a1i | |
14 | simpr | |
|
15 | 13 14 | fsnd | |
16 | snex | |
|
17 | 16 | a1i | |
18 | elmapg | |
|
19 | 17 18 | sylan2 | |
20 | 15 19 | mpbird | |
21 | fvexd | |
|
22 | 2 12 20 21 | fvmptd | |