Metamath Proof Explorer


Theorem s2f1o

Description: A length 2 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 s2f1o A S B S A B E = ⟨“ AB ”⟩ E : 0 1 1-1 onto A B

Proof

Step Hyp Ref Expression
1 simpl1 A S B S A B E = ⟨“ AB ”⟩ A S
2 0z 0
3 1 2 jctil A S B S A B E = ⟨“ AB ”⟩ 0 A S
4 simpl2 A S B S A B E = ⟨“ AB ”⟩ B S
5 1z 1
6 4 5 jctil A S B S A B E = ⟨“ AB ”⟩ 1 B S
7 3 6 jca A S B S A B E = ⟨“ AB ”⟩ 0 A S 1 B S
8 simpl3 A S B S A B E = ⟨“ AB ”⟩ A B
9 0ne1 0 1
10 8 9 jctil A S B S A B E = ⟨“ AB ”⟩ 0 1 A B
11 f1oprg 0 A S 1 B S 0 1 A B 0 A 1 B : 0 1 1-1 onto A B
12 7 10 11 sylc A S B S A B E = ⟨“ AB ”⟩ 0 A 1 B : 0 1 1-1 onto A B
13 eqcom E = ⟨“ AB ”⟩ ⟨“ AB ”⟩ = E
14 s2prop A S B S ⟨“ AB ”⟩ = 0 A 1 B
15 14 3adant3 A S B S A B ⟨“ AB ”⟩ = 0 A 1 B
16 15 eqeq1d A S B S A B ⟨“ AB ”⟩ = E 0 A 1 B = E
17 13 16 syl5bb A S B S A B E = ⟨“ AB ”⟩ 0 A 1 B = E
18 17 biimpa A S B S A B E = ⟨“ AB ”⟩ 0 A 1 B = E
19 18 f1oeq1d A S B S A B E = ⟨“ AB ”⟩ 0 A 1 B : 0 1 1-1 onto A B E : 0 1 1-1 onto A B
20 12 19 mpbid A S B S A B E = ⟨“ AB ”⟩ E : 0 1 1-1 onto A B
21 20 ex A S B S A B E = ⟨“ AB ”⟩ E : 0 1 1-1 onto A B