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 N 0 S repeatS N =

Proof

Step Hyp Ref Expression
1 df-reps repeatS = s V , n 0 x 0 ..^ n s
2 ovex 0 ..^ n V
3 2 mptex x 0 ..^ n s V
4 1 3 dmmpo dom repeatS = V × 0
5 df-nel N 0 ¬ N 0
6 5 biimpi N 0 ¬ N 0
7 6 intnand N 0 ¬ S V N 0
8 ndmovg dom repeatS = V × 0 ¬ S V N 0 S repeatS N =
9 4 7 8 sylancr N 0 S repeatS N =