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 e/ NN0 -> ( S repeatS N ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		df-reps	|- repeatS = ( s e. _V , n e. NN0 |-> ( x e. ( 0 ..^ n ) |-> s ) )
2		ovex	|- ( 0 ..^ n ) e. _V
3	2	mptex	|- ( x e. ( 0 ..^ n ) |-> s ) e. _V
4	1 3	dmmpo	|- dom repeatS = ( _V X. NN0 )
5		df-nel	|- ( N e/ NN0 <-> -. N e. NN0 )
6	5	biimpi	|- ( N e/ NN0 -> -. N e. NN0 )
7	6	intnand	|- ( N e/ NN0 -> -. ( S e. _V /\ N e. NN0 ) )
8		ndmovg	|- ( ( dom repeatS = ( _V X. NN0 ) /\ -. ( S e. _V /\ N e. NN0 ) ) -> ( S repeatS N ) = (/) )
9	4 7 8	sylancr	|- ( N e/ NN0 -> ( S repeatS N ) = (/) )