Theorem repsw0

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

	Ref	Expression
Assertion	repsw0	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 repeatS 0 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		0nn0	⊢ 0 ∈ ℕ0
2		repswlen	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 0 ∈ ℕ0 ) → ( ♯ ‘ ( 𝑆 repeatS 0 ) ) = 0 )
3	1 2	mpan2	⊢ ( 𝑆 ∈ 𝑉 → ( ♯ ‘ ( 𝑆 repeatS 0 ) ) = 0 )
4		ovex	⊢ ( 𝑆 repeatS 0 ) ∈ V
5		hasheq0	⊢ ( ( 𝑆 repeatS 0 ) ∈ V → ( ( ♯ ‘ ( 𝑆 repeatS 0 ) ) = 0 ↔ ( 𝑆 repeatS 0 ) = ∅ ) )
6	4 5	mp1i	⊢ ( 𝑆 ∈ 𝑉 → ( ( ♯ ‘ ( 𝑆 repeatS 0 ) ) = 0 ↔ ( 𝑆 repeatS 0 ) = ∅ ) )
7	3 6	mpbid	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 repeatS 0 ) = ∅ )