Metamath Proof Explorer

Theorem s4f1o

Description: A length 4 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 s4f1o 
|- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( E = <" A B C D "> -> E : dom E -1-1-onto-> ( { A , B } u. { C , D } ) ) ) )

Proof

Step Hyp Ref Expression
1 f1oun2prg 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) ) )
2 1 imp 
 |-  ( ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) )
3 2 adantr 
 |-  ( ( ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) /\ E = <" A B C D "> ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) )
4 s4prop 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> <" A B C D "> = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) )
5 4 adantr 
 |-  ( ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> <" A B C D "> = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) )
6 5 eqeq2d 
 |-  ( ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( E = <" A B C D "> <-> E = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) ) )
7 6 biimpa 
 |-  ( ( ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) /\ E = <" A B C D "> ) -> E = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) )
8 7 eqcomd 
 |-  ( ( ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) /\ E = <" A B C D "> ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) = E )
9 8 f1oeq1d 
 |-  ( ( ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) /\ E = <" A B C D "> ) -> ( ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) <-> E : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) ) )
10 3 9 mpbid 
 |-  ( ( ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) /\ E = <" A B C D "> ) -> E : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) )
11 dff1o5 
 |-  ( E : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) <-> ( E : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-> ( { A , B } u. { C , D } ) /\ ran E = ( { A , B } u. { C , D } ) ) )
12 dff12 
 |-  ( E : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-> ( { A , B } u. { C , D } ) <-> ( E : ( { 0 , 1 } u. { 2 , 3 } ) --> ( { A , B } u. { C , D } ) /\ A. y E* x x E y ) )
13 12 bicomi 
 |-  ( ( E : ( { 0 , 1 } u. { 2 , 3 } ) --> ( { A , B } u. { C , D } ) /\ A. y E* x x E y ) <-> E : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-> ( { A , B } u. { C , D } ) )
14 13 anbi1i 
 |-  ( ( ( E : ( { 0 , 1 } u. { 2 , 3 } ) --> ( { A , B } u. { C , D } ) /\ A. y E* x x E y ) /\ ran E = ( { A , B } u. { C , D } ) ) <-> ( E : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-> ( { A , B } u. { C , D } ) /\ ran E = ( { A , B } u. { C , D } ) ) )
15 11 14 sylbb2 
 |-  ( E : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) -> ( ( E : ( { 0 , 1 } u. { 2 , 3 } ) --> ( { A , B } u. { C , D } ) /\ A. y E* x x E y ) /\ ran E = ( { A , B } u. { C , D } ) ) )
16 ffdm 
 |-  ( E : ( { 0 , 1 } u. { 2 , 3 } ) --> ( { A , B } u. { C , D } ) -> ( E : dom E --> ( { A , B } u. { C , D } ) /\ dom E C_ ( { 0 , 1 } u. { 2 , 3 } ) ) )
17 16 simpld 
 |-  ( E : ( { 0 , 1 } u. { 2 , 3 } ) --> ( { A , B } u. { C , D } ) -> E : dom E --> ( { A , B } u. { C , D } ) )
18 17 anim1i 
 |-  ( ( E : ( { 0 , 1 } u. { 2 , 3 } ) --> ( { A , B } u. { C , D } ) /\ A. y E* x x E y ) -> ( E : dom E --> ( { A , B } u. { C , D } ) /\ A. y E* x x E y ) )
19 18 anim1i 
 |-  ( ( ( E : ( { 0 , 1 } u. { 2 , 3 } ) --> ( { A , B } u. { C , D } ) /\ A. y E* x x E y ) /\ ran E = ( { A , B } u. { C , D } ) ) -> ( ( E : dom E --> ( { A , B } u. { C , D } ) /\ A. y E* x x E y ) /\ ran E = ( { A , B } u. { C , D } ) ) )
20 15 19 syl 
 |-  ( E : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) -> ( ( E : dom E --> ( { A , B } u. { C , D } ) /\ A. y E* x x E y ) /\ ran E = ( { A , B } u. { C , D } ) ) )
21 dff12 
 |-  ( E : dom E -1-1-> ( { A , B } u. { C , D } ) <-> ( E : dom E --> ( { A , B } u. { C , D } ) /\ A. y E* x x E y ) )
22 21 anbi1i 
 |-  ( ( E : dom E -1-1-> ( { A , B } u. { C , D } ) /\ ran E = ( { A , B } u. { C , D } ) ) <-> ( ( E : dom E --> ( { A , B } u. { C , D } ) /\ A. y E* x x E y ) /\ ran E = ( { A , B } u. { C , D } ) ) )
23 20 22 sylibr 
 |-  ( E : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) -> ( E : dom E -1-1-> ( { A , B } u. { C , D } ) /\ ran E = ( { A , B } u. { C , D } ) ) )
24 dff1o5 
 |-  ( E : dom E -1-1-onto-> ( { A , B } u. { C , D } ) <-> ( E : dom E -1-1-> ( { A , B } u. { C , D } ) /\ ran E = ( { A , B } u. { C , D } ) ) )
25 23 24 sylibr 
 |-  ( E : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) -> E : dom E -1-1-onto-> ( { A , B } u. { C , D } ) )
26 10 25 syl 
 |-  ( ( ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) /\ E = <" A B C D "> ) -> E : dom E -1-1-onto-> ( { A , B } u. { C , D } ) )
27 26 exp31 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( E = <" A B C D "> -> E : dom E -1-1-onto-> ( { A , B } u. { C , D } ) ) ) )