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

Metamath Proof Explorer

Theorem s7f1o

Description: A length 7 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by AV, 2-Aug-2025)

Ref Expression
Assertion s7f1o 
|- ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( K = <" A B C D E F G "> -> K : ( 0 ..^ 7 ) -1-1-onto-> ( ( { A , B , C } u. { D } ) u. { E , F , G } ) ) )

Proof

Step Hyp Ref Expression
1 s7cli 
 |-  <" A B C D E F G "> e. Word _V
2 wrdf 
 |-  ( <" A B C D E F G "> e. Word _V -> <" A B C D E F G "> : ( 0 ..^ ( # ` <" A B C D E F G "> ) ) --> _V )
3 s7len 
 |-  ( # ` <" A B C D E F G "> ) = 7
4 3 oveq2i 
 |-  ( 0 ..^ ( # ` <" A B C D E F G "> ) ) = ( 0 ..^ 7 )
5 4 feq2i 
 |-  ( <" A B C D E F G "> : ( 0 ..^ ( # ` <" A B C D E F G "> ) ) --> _V <-> <" A B C D E F G "> : ( 0 ..^ 7 ) --> _V )
6 ffn 
 |-  ( <" A B C D E F G "> : ( 0 ..^ 7 ) --> _V -> <" A B C D E F G "> Fn ( 0 ..^ 7 ) )
7 5 6 sylbi 
 |-  ( <" A B C D E F G "> : ( 0 ..^ ( # ` <" A B C D E F G "> ) ) --> _V -> <" A B C D E F G "> Fn ( 0 ..^ 7 ) )
8 1 2 7 mp2b 
 |-  <" A B C D E F G "> Fn ( 0 ..^ 7 )
9 8 a1i 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> <" A B C D E F G "> Fn ( 0 ..^ 7 ) )
10 dffn4 
 |-  ( <" A B C D E F G "> Fn ( 0 ..^ 7 ) <-> <" A B C D E F G "> : ( 0 ..^ 7 ) -onto-> ran <" A B C D E F G "> )
11 9 10 sylib 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> <" A B C D E F G "> : ( 0 ..^ 7 ) -onto-> ran <" A B C D E F G "> )
12 simp1 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> A e. V )
13 12 3ad2ant1 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> A e. V )
14 simp2 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> B e. V )
15 14 3ad2ant1 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> B e. V )
16 simp3 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> C e. V )
17 16 3ad2ant1 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> C e. V )
18 simp2 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> D e. V )
19 simp1 
 |-  ( ( E e. V /\ F e. V /\ G e. V ) -> E e. V )
20 19 3ad2ant3 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> E e. V )
21 simp2 
 |-  ( ( E e. V /\ F e. V /\ G e. V ) -> F e. V )
22 21 3ad2ant3 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> F e. V )
23 simp3 
 |-  ( ( E e. V /\ F e. V /\ G e. V ) -> G e. V )
24 23 3ad2ant3 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> G e. V )
25 13 15 17 18 20 22 24 s7rn 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> ran <" A B C D E F G "> = ( ( { A , B , C } u. { D } ) u. { E , F , G } ) )
26 foeq3 
 |-  ( ran <" A B C D E F G "> = ( ( { A , B , C } u. { D } ) u. { E , F , G } ) -> ( <" A B C D E F G "> : ( 0 ..^ 7 ) -onto-> ran <" A B C D E F G "> <-> <" A B C D E F G "> : ( 0 ..^ 7 ) -onto-> ( ( { A , B , C } u. { D } ) u. { E , F , G } ) ) )
27 25 26 syl 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> ( <" A B C D E F G "> : ( 0 ..^ 7 ) -onto-> ran <" A B C D E F G "> <-> <" A B C D E F G "> : ( 0 ..^ 7 ) -onto-> ( ( { A , B , C } u. { D } ) u. { E , F , G } ) ) )
28 11 27 mpbid 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> <" A B C D E F G "> : ( 0 ..^ 7 ) -onto-> ( ( { A , B , C } u. { D } ) u. { E , F , G } ) )
29 28 adantr 
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> <" A B C D E F G "> : ( 0 ..^ 7 ) -onto-> ( ( { A , B , C } u. { D } ) u. { E , F , G } ) )
30 7nn0 
 |-  7 e. NN0
31 hashfzo0 
 |-  ( 7 e. NN0 -> ( # ` ( 0 ..^ 7 ) ) = 7 )
32 30 31 ax-mp 
 |-  ( # ` ( 0 ..^ 7 ) ) = 7
33 hash7g 
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( # ` ( ( { A , B , C } u. { D } ) u. { E , F , G } ) ) = 7 )
34 32 33 eqtr4id 
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( # ` ( 0 ..^ 7 ) ) = ( # ` ( ( { A , B , C } u. { D } ) u. { E , F , G } ) ) )
35 fzofi 
 |-  ( 0 ..^ 7 ) e. Fin
36 tpfi 
 |-  { A , B , C } e. Fin
37 snfi 
 |-  { D } e. Fin
38 unfi 
 |-  ( ( { A , B , C } e. Fin /\ { D } e. Fin ) -> ( { A , B , C } u. { D } ) e. Fin )
39 36 37 38 mp2an 
 |-  ( { A , B , C } u. { D } ) e. Fin
40 tpfi 
 |-  { E , F , G } e. Fin
41 unfi 
 |-  ( ( ( { A , B , C } u. { D } ) e. Fin /\ { E , F , G } e. Fin ) -> ( ( { A , B , C } u. { D } ) u. { E , F , G } ) e. Fin )
42 39 40 41 mp2an 
 |-  ( ( { A , B , C } u. { D } ) u. { E , F , G } ) e. Fin
43 hashen 
 |-  ( ( ( 0 ..^ 7 ) e. Fin /\ ( ( { A , B , C } u. { D } ) u. { E , F , G } ) e. Fin ) -> ( ( # ` ( 0 ..^ 7 ) ) = ( # ` ( ( { A , B , C } u. { D } ) u. { E , F , G } ) ) <-> ( 0 ..^ 7 ) ~~ ( ( { A , B , C } u. { D } ) u. { E , F , G } ) ) )
44 35 42 43 mp2an 
 |-  ( ( # ` ( 0 ..^ 7 ) ) = ( # ` ( ( { A , B , C } u. { D } ) u. { E , F , G } ) ) <-> ( 0 ..^ 7 ) ~~ ( ( { A , B , C } u. { D } ) u. { E , F , G } ) )
45 34 44 sylib 
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( 0 ..^ 7 ) ~~ ( ( { A , B , C } u. { D } ) u. { E , F , G } ) )
46 42 a1i 
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( ( { A , B , C } u. { D } ) u. { E , F , G } ) e. Fin )
47 fofinf1o 
 |-  ( ( <" A B C D E F G "> : ( 0 ..^ 7 ) -onto-> ( ( { A , B , C } u. { D } ) u. { E , F , G } ) /\ ( 0 ..^ 7 ) ~~ ( ( { A , B , C } u. { D } ) u. { E , F , G } ) /\ ( ( { A , B , C } u. { D } ) u. { E , F , G } ) e. Fin ) -> <" A B C D E F G "> : ( 0 ..^ 7 ) -1-1-onto-> ( ( { A , B , C } u. { D } ) u. { E , F , G } ) )
48 29 45 46 47 syl3anc 
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> <" A B C D E F G "> : ( 0 ..^ 7 ) -1-1-onto-> ( ( { A , B , C } u. { D } ) u. { E , F , G } ) )
49 f1oeq1 
 |-  ( K = <" A B C D E F G "> -> ( K : ( 0 ..^ 7 ) -1-1-onto-> ( ( { A , B , C } u. { D } ) u. { E , F , G } ) <-> <" A B C D E F G "> : ( 0 ..^ 7 ) -1-1-onto-> ( ( { A , B , C } u. { D } ) u. { E , F , G } ) ) )
50 48 49 syl5ibrcom 
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( K = <" A B C D E F G "> -> K : ( 0 ..^ 7 ) -1-1-onto-> ( ( { A , B , C } u. { D } ) u. { E , F , G } ) ) )