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 eqidd 
 |-  ( ( ( ( ( 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 , 1 } u. { 2 , 3 } ) = ( { 0 , 1 } u. { 2 , 3 } ) )
10 eqidd 
 |-  ( ( ( ( ( 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 "> ) -> ( { A , B } u. { C , D } ) = ( { A , B } u. { C , D } ) )
11 8 9 10 f1oeq123d 
 |-  ( ( ( ( ( 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 } ) ) )
12 3 11 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 } ) )
13 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 } ) ) )
14 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 ) )
15 14 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 } ) )
16 15 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 } ) ) )
17 13 16 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 } ) ) )
18 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 } ) ) )
19 18 simpld 
 |-  ( E : ( { 0 , 1 } u. { 2 , 3 } ) --> ( { A , B } u. { C , D } ) -> E : dom E --> ( { A , B } u. { C , D } ) )
20 19 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 ) )
21 20 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 } ) ) )
22 17 21 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 } ) ) )
23 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 ) )
24 23 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 } ) ) )
25 22 24 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 } ) ) )
26 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 } ) ) )
27 25 26 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 } ) )
28 12 27 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 } ) )
29 28 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 } ) ) ) )