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