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 ℕ_{0} \to S repeatS N = \emptyset$

Proof

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

Metamath Proof Explorer

Theorem repsundef

Proof