This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀ ) → ( 𝑆 repeatS 𝑁 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 ∈ 𝑉 )
2	1	ralrimiva	⊢ ( 𝑆 ∈ 𝑉 → ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) 𝑆 ∈ 𝑉 )
3	2	adantr	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀ ) → ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) 𝑆 ∈ 𝑉 )
4		eqid	⊢ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 )
5	4	fmpt	⊢ ( ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) 𝑆 ∈ 𝑉 ↔ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑉 )
6	3 5	sylib	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀ ) → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑉 )
7		reps	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀ ) → ( 𝑆 repeatS 𝑁 ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) )
8	7	feq1d	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀ ) → ( ( 𝑆 repeatS 𝑁 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑉 ↔ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑉 ) )
9	6 8	mpbird	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀ ) → ( 𝑆 repeatS 𝑁 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑉 )