Description: A function mapping a half-open range of nonnegative integers with an upper bound not being a nonnegative integer to a constant is the empty set (in the meaning of "undefined"). (Contributed by AV, 5-Nov-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | repsundef | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-reps | |
|
2 | ovex | |
|
3 | 2 | mptex | |
4 | 1 3 | dmmpo | |
5 | df-nel | |
|
6 | 5 | biimpi | |
7 | 6 | intnand | |
8 | ndmovg | |
|
9 | 4 7 8 | sylancr | |