Theorem repsw1

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

	Ref	Expression
Assertion	repsw1	$$⊢S\in V\to S\mathrm{repeatS}1=⟨“S”⟩$$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2		repsconst	$$⊢\left(S\in V\wedge 1\in {\mathbb{N}}_0\right)\to S\mathrm{repeatS}1=\left(0..^1\right)\times \left\{S\right\}$$
3	1 2	mpan2	$$⊢S\in V\to S\mathrm{repeatS}1=\left(0..^1\right)\times \left\{S\right\}$$
4		fzo01	$$⊢\left(0..^1\right)=\left\{0\right\}$$
5	4	a1i	$$⊢S\in V\to \left(0..^1\right)=\left\{0\right\}$$
6	5	xpeq1d	$$⊢S\in V\to \left(0..^1\right)\times \left\{S\right\}=\left\{0\right\}\times \left\{S\right\}$$
7		c0ex	$$⊢0\in \mathrm{V}$$
8		xpsng	$$⊢\left(0\in \mathrm{V}\wedge S\in V\right)\to \left\{0\right\}\times \left\{S\right\}=\left\{⟨0,S⟩\right\}$$
9	7 8	mpan	$$⊢S\in V\to \left\{0\right\}\times \left\{S\right\}=\left\{⟨0,S⟩\right\}$$
10	3 6 9	3eqtrd	$$⊢S\in V\to S\mathrm{repeatS}1=\left\{⟨0,S⟩\right\}$$
11		s1val	$$⊢S\in V\to ⟨“S”⟩=\left\{⟨0,S⟩\right\}$$
12	10 11	eqtr4d	$$⊢S\in V\to S\mathrm{repeatS}1=⟨“S”⟩$$