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

Metamath Proof Explorer

Theorem repsw1

Description: The "repeated symbol word" of length 1. (Contributed by AV, 4-Nov-2018)

Ref Expression
Assertion repsw1 ( 𝑆 ∈ 𝑉 → ( 𝑆 repeatS 1 ) = ⟨“ 𝑆 ”⟩ )

Proof

Step Hyp Ref Expression
1 1nn0 ⊢ 1 ∈ ℕ0
2 repsconst ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 1 ∈ ℕ0 ) → ( 𝑆 repeatS 1 ) = ( ( 0 ..^ 1 ) × { 𝑆 } ) )
3 1 2 mpan2 ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 repeatS 1 ) = ( ( 0 ..^ 1 ) × { 𝑆 } ) )
4 fzo01 ⊢ ( 0 ..^ 1 ) = { 0 }
5 4 a1i ⊢ ( 𝑆 ∈ 𝑉 → ( 0 ..^ 1 ) = { 0 } )
6 5 xpeq1d ⊢ ( 𝑆 ∈ 𝑉 → ( ( 0 ..^ 1 ) × { 𝑆 } ) = ( { 0 } × { 𝑆 } ) )
7 c0ex ⊢ 0 ∈ V
8 xpsng ⊢ ( ( 0 ∈ V ∧ 𝑆 ∈ 𝑉 ) → ( { 0 } × { 𝑆 } ) = { ⟨ 0 , 𝑆 ⟩ } )
9 7 8 mpan ⊢ ( 𝑆 ∈ 𝑉 → ( { 0 } × { 𝑆 } ) = { ⟨ 0 , 𝑆 ⟩ } )
10 3 6 9 3eqtrd ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 repeatS 1 ) = { ⟨ 0 , 𝑆 ⟩ } )
11 s1val ⊢ ( 𝑆 ∈ 𝑉 → ⟨“ 𝑆 ”⟩ = { ⟨ 0 , 𝑆 ⟩ } )
12 10 11 eqtr4d ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 repeatS 1 ) = ⟨“ 𝑆 ”⟩ )