Metamath Proof Explorer


Theorem repsundef

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 N0SrepeatSN=

Proof

Step Hyp Ref Expression
1 df-reps repeatS=sV,n0x0..^ns
2 ovex 0..^nV
3 2 mptex x0..^nsV
4 1 3 dmmpo domrepeatS=V×0
5 df-nel N0¬N0
6 5 biimpi N0¬N0
7 6 intnand N0¬SVN0
8 ndmovg domrepeatS=V×0¬SVN0SrepeatSN=
9 4 7 8 sylancr N0SrepeatSN=