Metamath Proof Explorer

Theorem repsw0

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

Ref Expression
Assertion repsw0 
|- ( S e. V -> ( S repeatS 0 ) = (/) )

Proof

Step Hyp Ref Expression
1 0nn0 
 |-  0 e. NN0
2 repswlen 
 |-  ( ( S e. V /\ 0 e. NN0 ) -> ( # ` ( S repeatS 0 ) ) = 0 )
3 1 2 mpan2 
 |-  ( S e. V -> ( # ` ( S repeatS 0 ) ) = 0 )
4 ovex 
 |-  ( S repeatS 0 ) e. _V
5 hasheq0 
 |-  ( ( S repeatS 0 ) e. _V -> ( ( # ` ( S repeatS 0 ) ) = 0 <-> ( S repeatS 0 ) = (/) ) )
6 4 5 mp1i 
 |-  ( S e. V -> ( ( # ` ( S repeatS 0 ) ) = 0 <-> ( S repeatS 0 ) = (/) ) )
7 3 6 mpbid 
 |-  ( S e. V -> ( S repeatS 0 ) = (/) )