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 ) = ⟨“ 𝑆 ”⟩ )