Metamath Proof Explorer

Theorem repsf

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

		Ref	Expression
	Assertion	repsf	$⊢ (S \in V \land N \in ℕ_{0}) \to (S repeatS N) : (0 ..^N) ⟶ V$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (S \in V \land x \in (0 ..^N)) \to S \in V$
2	1	ralrimiva	$⊢ S \in V \to \forall x \in (0 ..^N) S \in V$
3	2	adantr	$⊢ (S \in V \land N \in ℕ_{0}) \to \forall x \in (0 ..^N) S \in V$
4		eqid	$⊢ (x \in (0 ..^N) ⟼ S) = (x \in (0 ..^N) ⟼ S)$
5	4	fmpt	$⊢ \forall x \in (0 ..^N) S \in V \leftrightarrow (x \in (0 ..^N) ⟼ S) : (0 ..^N) ⟶ V$
6	3 5	sylib	$⊢ (S \in V \land N \in ℕ_{0}) \to (x \in (0 ..^N) ⟼ S) : (0 ..^N) ⟶ V$
7		reps	$⊢ (S \in V \land N \in ℕ_{0}) \to S repeatS N = (x \in (0 ..^N) ⟼ S)$
8	7	feq1d	$⊢ (S \in V \land N \in ℕ_{0}) \to ((S repeatS N) : (0 ..^N) ⟶ V \leftrightarrow (x \in (0 ..^N) ⟼ S) : (0 ..^N) ⟶ V)$
9	6 8	mpbird	$⊢ (S \in V \land N \in ℕ_{0}) \to (S repeatS N) : (0 ..^N) ⟶ V$