reps

Description: Construct a function mapping a half-open range of nonnegative integers to a constant. (Contributed by AV, 4-Nov-2018)

		Ref	Expression
	Assertion	reps	$⊢ (S \in V \land N \in ℕ_{0}) \to S repeatS N = (x \in (0 ..^N) ⟼ S)$

Step	Hyp	Ref	Expression
1		elex	$⊢ S \in V \to S \in V$
2	1	adantr	$⊢ (S \in V \land N \in ℕ_{0}) \to S \in V$
3		simpr	$⊢ (S \in V \land N \in ℕ_{0}) \to N \in ℕ_{0}$
4		ovex	$⊢ (0 ..^N) \in V$
5		mptexg	$⊢ (0 ..^N) \in V \to (x \in (0 ..^N) ⟼ S) \in V$
6	4 5	mp1i	$⊢ (S \in V \land N \in ℕ_{0}) \to (x \in (0 ..^N) ⟼ S) \in V$
7		oveq2	$⊢ n = N \to (0 ..^n) = (0 ..^N)$
8	7	adantl	$⊢ (s = S \land n = N) \to (0 ..^n) = (0 ..^N)$
9		simpll	$⊢ ((s = S \land n = N) \land x \in (0 ..^n)) \to s = S$
10	8 9	mpteq12dva	$⊢ (s = S \land n = N) \to (x \in (0 ..^n) ⟼ s) = (x \in (0 ..^N) ⟼ S)$
11		df-reps	$⊢ repeatS = (s \in V, n \in ℕ_{0} ⟼ (x \in (0 ..^n) ⟼ s))$
12	10 11	ovmpoga	$⊢ (S \in V \land N \in ℕ_{0} \land (x \in (0 ..^N) ⟼ S) \in V) \to S repeatS N = (x \in (0 ..^N) ⟼ S)$
13	2 3 6 12	syl3anc	$⊢ (S \in V \land N \in ℕ_{0}) \to S repeatS N = (x \in (0 ..^N) ⟼ S)$

Metamath Proof Explorer