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\notin {\mathbb{N}}_0\to S\mathrm{repeatS}N=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-reps	$$⊢\mathrm{repeatS}=\left(s\in \mathrm{V},n\in {\mathbb{N}}_0⟼\left(x\in \left(0..^n\right)⟼s\right)\right)$$
2		ovex	$$⊢\left(0..^n\right)\in \mathrm{V}$$
3	2	mptex	$$⊢\left(x\in \left(0..^n\right)⟼s\right)\in \mathrm{V}$$
4	1 3	dmmpo	$$⊢\mathrm{dom}\mathrm{repeatS}=\mathrm{V}\times {\mathbb{N}}_0$$
5		df-nel	$$⊢N\notin {\mathbb{N}}_0\leftrightarrow \neg N\in {\mathbb{N}}_0$$
6	5	biimpi	$$⊢N\notin {\mathbb{N}}_0\to \neg N\in {\mathbb{N}}_0$$
7	6	intnand	$$⊢N\notin {\mathbb{N}}_0\to \neg \left(S\in \mathrm{V}\wedge N\in {\mathbb{N}}_0\right)$$
8		ndmovg	$$⊢\left(\mathrm{dom}\mathrm{repeatS}=\mathrm{V}\times {\mathbb{N}}_0\wedge \neg \left(S\in \mathrm{V}\wedge N\in {\mathbb{N}}_0\right)\right)\to S\mathrm{repeatS}N=\varnothing$$
9	4 7 8	sylancr	$$⊢N\notin {\mathbb{N}}_0\to S\mathrm{repeatS}N=\varnothing$$