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 ASBSCSDSABACADBCBDCDE=⟨“ABCD”⟩E:domE1-1 ontoABCD

Proof

Step Hyp Ref Expression
1 f1oun2prg ASBSCSDSABACADBCBDCD0A1B2C3D:01231-1 ontoABCD
2 1 imp ASBSCSDSABACADBCBDCD0A1B2C3D:01231-1 ontoABCD
3 2 adantr ASBSCSDSABACADBCBDCDE=⟨“ABCD”⟩0A1B2C3D:01231-1 ontoABCD
4 s4prop ASBSCSDS⟨“ABCD”⟩=0A1B2C3D
5 4 adantr ASBSCSDSABACADBCBDCD⟨“ABCD”⟩=0A1B2C3D
6 5 eqeq2d ASBSCSDSABACADBCBDCDE=⟨“ABCD”⟩E=0A1B2C3D
7 6 biimpa ASBSCSDSABACADBCBDCDE=⟨“ABCD”⟩E=0A1B2C3D
8 7 eqcomd ASBSCSDSABACADBCBDCDE=⟨“ABCD”⟩0A1B2C3D=E
9 8 f1oeq1d ASBSCSDSABACADBCBDCDE=⟨“ABCD”⟩0A1B2C3D:01231-1 ontoABCDE:01231-1 ontoABCD
10 3 9 mpbid ASBSCSDSABACADBCBDCDE=⟨“ABCD”⟩E:01231-1 ontoABCD
11 dff1o5 E:01231-1 ontoABCDE:01231-1ABCDranE=ABCD
12 dff12 E:01231-1ABCDE:0123ABCDy*xxEy
13 12 bicomi E:0123ABCDy*xxEyE:01231-1ABCD
14 13 anbi1i E:0123ABCDy*xxEyranE=ABCDE:01231-1ABCDranE=ABCD
15 11 14 sylbb2 E:01231-1 ontoABCDE:0123ABCDy*xxEyranE=ABCD
16 ffdm E:0123ABCDE:domEABCDdomE0123
17 16 simpld E:0123ABCDE:domEABCD
18 17 anim1i E:0123ABCDy*xxEyE:domEABCDy*xxEy
19 18 anim1i E:0123ABCDy*xxEyranE=ABCDE:domEABCDy*xxEyranE=ABCD
20 15 19 syl E:01231-1 ontoABCDE:domEABCDy*xxEyranE=ABCD
21 dff12 E:domE1-1ABCDE:domEABCDy*xxEy
22 21 anbi1i E:domE1-1ABCDranE=ABCDE:domEABCDy*xxEyranE=ABCD
23 20 22 sylibr E:01231-1 ontoABCDE:domE1-1ABCDranE=ABCD
24 dff1o5 E:domE1-1 ontoABCDE:domE1-1ABCDranE=ABCD
25 23 24 sylibr E:01231-1 ontoABCDE:domE1-1 ontoABCD
26 10 25 syl ASBSCSDSABACADBCBDCDE=⟨“ABCD”⟩E:domE1-1 ontoABCD
27 26 exp31 ASBSCSDSABACADBCBDCDE=⟨“ABCD”⟩E:domE1-1 ontoABCD