Description: Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | snelmap.a | |
|
snelmap.b | |
||
snelmap.n | |
||
snelmap.e | |
||
Assertion | snelmap | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snelmap.a | |
|
2 | snelmap.b | |
|
3 | snelmap.n | |
|
4 | snelmap.e | |
|
5 | n0 | |
|
6 | 3 5 | sylib | |
7 | vex | |
|
8 | 7 | fvconst2 | |
9 | 8 | eqcomd | |
10 | 9 | adantl | |
11 | elmapg | |
|
12 | 2 1 11 | syl2anc | |
13 | 4 12 | mpbid | |
14 | 13 | adantr | |
15 | simpr | |
|
16 | 14 15 | ffvelrnd | |
17 | 10 16 | eqeltrd | |
18 | 17 | ex | |
19 | 18 | exlimdv | |
20 | 6 19 | mpd | |