Theorem repsw0

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

	Ref	Expression
Assertion	repsw0	$$⊢S\in V\to S\mathrm{repeatS}0=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0nn0	$$⊢0\in {\mathbb{N}}_0$$
2		repswlen	$$⊢\left(S\in V\wedge 0\in {\mathbb{N}}_0\right)\to \left|S\mathrm{repeatS}0\right|=0$$
3	1 2	mpan2	$$⊢S\in V\to \left|S\mathrm{repeatS}0\right|=0$$
4		ovex	$$⊢S\mathrm{repeatS}0\in \mathrm{V}$$
5		hasheq0	$$⊢S\mathrm{repeatS}0\in \mathrm{V}\to \left(\left|S\mathrm{repeatS}0\right|=0\leftrightarrow S\mathrm{repeatS}0=\varnothing \right)$$
6	4 5	mp1i	$$⊢S\in V\to \left(\left|S\mathrm{repeatS}0\right|=0\leftrightarrow S\mathrm{repeatS}0=\varnothing \right)$$
7	3 6	mpbid	$$⊢S\in V\to S\mathrm{repeatS}0=\varnothing$$