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

Metamath Proof Explorer

Theorem s1f1

Description: Conditions for a length 1 string to be a one-to-one function. (Contributed by Thierry Arnoux, 11-Dec-2023)

Ref Expression
Hypothesis s1f1.1 
|- ( ph -> I e. D )
Assertion s1f1 
|- ( ph -> <" I "> : dom <" I "> -1-1-> D )

Proof

Step Hyp Ref Expression
1 s1f1.1 
 |-  ( ph -> I e. D )
2 0nn0 
 |-  0 e. NN0
3 2 a1i 
 |-  ( ph -> 0 e. NN0 )
4 f1osng 
 |-  ( ( 0 e. NN0 /\ I e. D ) -> { <. 0 , I >. } : { 0 } -1-1-onto-> { I } )
5 3 1 4 syl2anc 
 |-  ( ph -> { <. 0 , I >. } : { 0 } -1-1-onto-> { I } )
6 f1of1 
 |-  ( { <. 0 , I >. } : { 0 } -1-1-onto-> { I } -> { <. 0 , I >. } : { 0 } -1-1-> { I } )
7 5 6 syl 
 |-  ( ph -> { <. 0 , I >. } : { 0 } -1-1-> { I } )
8 1 snssd 
 |-  ( ph -> { I } C_ D )
9 f1ss 
 |-  ( ( { <. 0 , I >. } : { 0 } -1-1-> { I } /\ { I } C_ D ) -> { <. 0 , I >. } : { 0 } -1-1-> D )
10 7 8 9 syl2anc 
 |-  ( ph -> { <. 0 , I >. } : { 0 } -1-1-> D )
11 s1val 
 |-  ( I e. D -> <" I "> = { <. 0 , I >. } )
12 1 11 syl 
 |-  ( ph -> <" I "> = { <. 0 , I >. } )
13 s1dm 
 |-  dom <" I "> = { 0 }
14 13 a1i 
 |-  ( ph -> dom <" I "> = { 0 } )
15 eqidd 
 |-  ( ph -> D = D )
16 12 14 15 f1eq123d 
 |-  ( ph -> ( <" I "> : dom <" I "> -1-1-> D <-> { <. 0 , I >. } : { 0 } -1-1-> D ) )
17 10 16 mpbird 
 |-  ( ph -> <" I "> : dom <" I "> -1-1-> D )