This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem repsw1

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

Ref Expression
Assertion repsw1 
|- ( S e. V -> ( S repeatS 1 ) = <" S "> )

Proof

Step Hyp Ref Expression
1 1nn0 
 |-  1 e. NN0
2 repsconst 
 |-  ( ( S e. V /\ 1 e. NN0 ) -> ( S repeatS 1 ) = ( ( 0 ..^ 1 ) X. { S } ) )
3 1 2 mpan2 
 |-  ( S e. V -> ( S repeatS 1 ) = ( ( 0 ..^ 1 ) X. { S } ) )
4 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
5 4 a1i 
 |-  ( S e. V -> ( 0 ..^ 1 ) = { 0 } )
6 5 xpeq1d 
 |-  ( S e. V -> ( ( 0 ..^ 1 ) X. { S } ) = ( { 0 } X. { S } ) )
7 c0ex 
 |-  0 e. _V
8 xpsng 
 |-  ( ( 0 e. _V /\ S e. V ) -> ( { 0 } X. { S } ) = { <. 0 , S >. } )
9 7 8 mpan 
 |-  ( S e. V -> ( { 0 } X. { S } ) = { <. 0 , S >. } )
10 3 6 9 3eqtrd 
 |-  ( S e. V -> ( S repeatS 1 ) = { <. 0 , S >. } )
11 s1val 
 |-  ( S e. V -> <" S "> = { <. 0 , S >. } )
12 10 11 eqtr4d 
 |-  ( S e. V -> ( S repeatS 1 ) = <" S "> )