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

Metamath Proof Explorer

Theorem s2f1

Description: Conditions for a length 2 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Hypotheses s2f1.i 
|- ( ph -> I e. D )
s2f1.j 
|- ( ph -> J e. D )
s2f1.1 
|- ( ph -> I =/= J )
Assertion s2f1 
|- ( ph -> <" I J "> : dom <" I J "> -1-1-> D )

Proof

Step Hyp Ref Expression
1 s2f1.i 
 |-  ( ph -> I e. D )
2 s2f1.j 
 |-  ( ph -> J e. D )
3 s2f1.1 
 |-  ( ph -> I =/= J )
4 0nn0 
 |-  0 e. NN0
5 4 a1i 
 |-  ( ph -> 0 e. NN0 )
6 1nn0 
 |-  1 e. NN0
7 6 a1i 
 |-  ( ph -> 1 e. NN0 )
8 0ne1 
 |-  0 =/= 1
9 8 a1i 
 |-  ( ph -> 0 =/= 1 )
10 f1oprg 
 |-  ( ( ( 0 e. NN0 /\ I e. D ) /\ ( 1 e. NN0 /\ J e. D ) ) -> ( ( 0 =/= 1 /\ I =/= J ) -> { <. 0 , I >. , <. 1 , J >. } : { 0 , 1 } -1-1-onto-> { I , J } ) )
11 10 3impia 
 |-  ( ( ( 0 e. NN0 /\ I e. D ) /\ ( 1 e. NN0 /\ J e. D ) /\ ( 0 =/= 1 /\ I =/= J ) ) -> { <. 0 , I >. , <. 1 , J >. } : { 0 , 1 } -1-1-onto-> { I , J } )
12 5 1 7 2 9 3 11 syl222anc 
 |-  ( ph -> { <. 0 , I >. , <. 1 , J >. } : { 0 , 1 } -1-1-onto-> { I , J } )
13 s2prop 
 |-  ( ( I e. D /\ J e. D ) -> <" I J "> = { <. 0 , I >. , <. 1 , J >. } )
14 1 2 13 syl2anc 
 |-  ( ph -> <" I J "> = { <. 0 , I >. , <. 1 , J >. } )
15 14 f1oeq1d 
 |-  ( ph -> ( <" I J "> : { 0 , 1 } -1-1-onto-> { I , J } <-> { <. 0 , I >. , <. 1 , J >. } : { 0 , 1 } -1-1-onto-> { I , J } ) )
16 12 15 mpbird 
 |-  ( ph -> <" I J "> : { 0 , 1 } -1-1-onto-> { I , J } )
17 f1of1 
 |-  ( <" I J "> : { 0 , 1 } -1-1-onto-> { I , J } -> <" I J "> : { 0 , 1 } -1-1-> { I , J } )
18 16 17 syl 
 |-  ( ph -> <" I J "> : { 0 , 1 } -1-1-> { I , J } )
19 1 2 prssd 
 |-  ( ph -> { I , J } C_ D )
20 f1ss 
 |-  ( ( <" I J "> : { 0 , 1 } -1-1-> { I , J } /\ { I , J } C_ D ) -> <" I J "> : { 0 , 1 } -1-1-> D )
21 18 19 20 syl2anc 
 |-  ( ph -> <" I J "> : { 0 , 1 } -1-1-> D )
22 f1dm 
 |-  ( <" I J "> : { 0 , 1 } -1-1-> D -> dom <" I J "> = { 0 , 1 } )
23 21 22 syl 
 |-  ( ph -> dom <" I J "> = { 0 , 1 } )
24 f1eq2 
 |-  ( dom <" I J "> = { 0 , 1 } -> ( <" I J "> : dom <" I J "> -1-1-> D <-> <" I J "> : { 0 , 1 } -1-1-> D ) )
25 23 24 syl 
 |-  ( ph -> ( <" I J "> : dom <" I J "> -1-1-> D <-> <" I J "> : { 0 , 1 } -1-1-> D ) )
26 21 25 mpbird 
 |-  ( ph -> <" I J "> : dom <" I J "> -1-1-> D )