Metamath Proof Explorer

Theorem s1len

Description: Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s1len 
|- ( # ` <" A "> ) = 1

Proof

Step Hyp Ref Expression
1 df-s1 
 |-  <" A "> = { <. 0 , ( _I ` A ) >. }
2 1 fveq2i 
 |-  ( # ` <" A "> ) = ( # ` { <. 0 , ( _I ` A ) >. } )
3 opex 
 |-  <. 0 , ( _I ` A ) >. e. _V
4 hashsng 
 |-  ( <. 0 , ( _I ` A ) >. e. _V -> ( # ` { <. 0 , ( _I ` A ) >. } ) = 1 )
5 3 4 ax-mp 
 |-  ( # ` { <. 0 , ( _I ` A ) >. } ) = 1
6 2 5 eqtri 
 |-  ( # ` <" A "> ) = 1