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 )