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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1oun2prg | |
|
2 | 1 | imp | |
3 | 2 | adantr | |
4 | s4prop | |
|
5 | 4 | adantr | |
6 | 5 | eqeq2d | |
7 | 6 | biimpa | |
8 | 7 | eqcomd | |
9 | 8 | f1oeq1d | |
10 | 3 9 | mpbid | |
11 | dff1o5 | |
|
12 | dff12 | |
|
13 | 12 | bicomi | |
14 | 13 | anbi1i | |
15 | 11 14 | sylbb2 | |
16 | ffdm | |
|
17 | 16 | simpld | |
18 | 17 | anim1i | |
19 | 18 | anim1i | |
20 | 15 19 | syl | |
21 | dff12 | |
|
22 | 21 | anbi1i | |
23 | 20 22 | sylibr | |
24 | dff1o5 | |
|
25 | 23 24 | sylibr | |
26 | 10 25 | syl | |
27 | 26 | exp31 | |