Metamath Proof Explorer

Theorem s2f1o

Description: A length 2 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by Alexander van der Vekens, 14-Aug-2017)

Ref Expression
Assertion s2f1o 
|- ( ( A e. S /\ B e. S /\ A =/= B ) -> ( E = <" A B "> -> E : { 0 , 1 } -1-1-onto-> { A , B } ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ E = <" A B "> ) -> A e. S )
2 0z 
 |-  0 e. ZZ
3 1 2 jctil 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ E = <" A B "> ) -> ( 0 e. ZZ /\ A e. S ) )
4 simpl2 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ E = <" A B "> ) -> B e. S )
5 1z 
 |-  1 e. ZZ
6 4 5 jctil 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ E = <" A B "> ) -> ( 1 e. ZZ /\ B e. S ) )
7 3 6 jca 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ E = <" A B "> ) -> ( ( 0 e. ZZ /\ A e. S ) /\ ( 1 e. ZZ /\ B e. S ) ) )
8 simpl3 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ E = <" A B "> ) -> A =/= B )
9 0ne1 
 |-  0 =/= 1
10 8 9 jctil 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ E = <" A B "> ) -> ( 0 =/= 1 /\ A =/= B ) )
11 f1oprg 
 |-  ( ( ( 0 e. ZZ /\ A e. S ) /\ ( 1 e. ZZ /\ B e. S ) ) -> ( ( 0 =/= 1 /\ A =/= B ) -> { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } -1-1-onto-> { A , B } ) )
12 7 10 11 sylc 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ E = <" A B "> ) -> { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } -1-1-onto-> { A , B } )
13 eqcom 
 |-  ( E = <" A B "> <-> <" A B "> = E )
14 s2prop 
 |-  ( ( A e. S /\ B e. S ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )
15 14 3adant3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )
16 15 eqeq1d 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( <" A B "> = E <-> { <. 0 , A >. , <. 1 , B >. } = E ) )
17 13 16 bitrid 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( E = <" A B "> <-> { <. 0 , A >. , <. 1 , B >. } = E ) )
18 17 biimpa 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ E = <" A B "> ) -> { <. 0 , A >. , <. 1 , B >. } = E )
19 18 f1oeq1d 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ E = <" A B "> ) -> ( { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } -1-1-onto-> { A , B } <-> E : { 0 , 1 } -1-1-onto-> { A , B } ) )
20 12 19 mpbid 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ E = <" A B "> ) -> E : { 0 , 1 } -1-1-onto-> { A , B } )
21 20 ex 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( E = <" A B "> -> E : { 0 , 1 } -1-1-onto-> { A , B } ) )