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 S B S C S D S A B A C A D B C B D C D E = ⟨“ ABCD ”⟩ E : dom E 1-1 onto A B C D

Proof

Step Hyp Ref Expression
1 f1oun2prg A S B S C S D S A B A C A D B C B D C D 0 A 1 B 2 C 3 D : 0 1 2 3 1-1 onto A B C D
2 1 imp A S B S C S D S A B A C A D B C B D C D 0 A 1 B 2 C 3 D : 0 1 2 3 1-1 onto A B C D
3 2 adantr A S B S C S D S A B A C A D B C B D C D E = ⟨“ ABCD ”⟩ 0 A 1 B 2 C 3 D : 0 1 2 3 1-1 onto A B C D
4 s4prop A S B S C S D S ⟨“ ABCD ”⟩ = 0 A 1 B 2 C 3 D
5 4 adantr A S B S C S D S A B A C A D B C B D C D ⟨“ ABCD ”⟩ = 0 A 1 B 2 C 3 D
6 5 eqeq2d A S B S C S D S A B A C A D B C B D C D E = ⟨“ ABCD ”⟩ E = 0 A 1 B 2 C 3 D
7 6 biimpa A S B S C S D S A B A C A D B C B D C D E = ⟨“ ABCD ”⟩ E = 0 A 1 B 2 C 3 D
8 7 eqcomd A S B S C S D S A B A C A D B C B D C D E = ⟨“ ABCD ”⟩ 0 A 1 B 2 C 3 D = E
9 8 f1oeq1d A S B S C S D S A B A C A D B C B D C D E = ⟨“ ABCD ”⟩ 0 A 1 B 2 C 3 D : 0 1 2 3 1-1 onto A B C D E : 0 1 2 3 1-1 onto A B C D
10 3 9 mpbid A S B S C S D S A B A C A D B C B D C D E = ⟨“ ABCD ”⟩ E : 0 1 2 3 1-1 onto A B C D
11 dff1o5 E : 0 1 2 3 1-1 onto A B C D E : 0 1 2 3 1-1 A B C D ran E = A B C D
12 dff12 E : 0 1 2 3 1-1 A B C D E : 0 1 2 3 A B C D y * x x E y
13 12 bicomi E : 0 1 2 3 A B C D y * x x E y E : 0 1 2 3 1-1 A B C D
14 13 anbi1i E : 0 1 2 3 A B C D y * x x E y ran E = A B C D E : 0 1 2 3 1-1 A B C D ran E = A B C D
15 11 14 sylbb2 E : 0 1 2 3 1-1 onto A B C D E : 0 1 2 3 A B C D y * x x E y ran E = A B C D
16 ffdm E : 0 1 2 3 A B C D E : dom E A B C D dom E 0 1 2 3
17 16 simpld E : 0 1 2 3 A B C D E : dom E A B C D
18 17 anim1i E : 0 1 2 3 A B C D y * x x E y E : dom E A B C D y * x x E y
19 18 anim1i E : 0 1 2 3 A B C D y * x x E y ran E = A B C D E : dom E A B C D y * x x E y ran E = A B C D
20 15 19 syl E : 0 1 2 3 1-1 onto A B C D E : dom E A B C D y * x x E y ran E = A B C D
21 dff12 E : dom E 1-1 A B C D E : dom E A B C D y * x x E y
22 21 anbi1i E : dom E 1-1 A B C D ran E = A B C D E : dom E A B C D y * x x E y ran E = A B C D
23 20 22 sylibr E : 0 1 2 3 1-1 onto A B C D E : dom E 1-1 A B C D ran E = A B C D
24 dff1o5 E : dom E 1-1 onto A B C D E : dom E 1-1 A B C D ran E = A B C D
25 23 24 sylibr E : 0 1 2 3 1-1 onto A B C D E : dom E 1-1 onto A B C D
26 10 25 syl A S B S C S D S A B A C A D B C B D C D E = ⟨“ ABCD ”⟩ E : dom E 1-1 onto A B C D
27 26 exp31 A S B S C S D S A B A C A D B C B D C D E = ⟨“ ABCD ”⟩ E : dom E 1-1 onto A B C D