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 ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) → ( 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ → 𝐸 : { 0 , 1 } –1-1-onto→ { 𝐴 , 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 simpl1 ( ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → 𝐴𝑆 )
2 0z 0 ∈ ℤ
3 1 2 jctil ( ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → ( 0 ∈ ℤ ∧ 𝐴𝑆 ) )
4 simpl2 ( ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → 𝐵𝑆 )
5 1z 1 ∈ ℤ
6 4 5 jctil ( ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → ( 1 ∈ ℤ ∧ 𝐵𝑆 ) )
7 3 6 jca ( ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → ( ( 0 ∈ ℤ ∧ 𝐴𝑆 ) ∧ ( 1 ∈ ℤ ∧ 𝐵𝑆 ) ) )
8 simpl3 ( ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → 𝐴𝐵 )
9 0ne1 0 ≠ 1
10 8 9 jctil ( ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → ( 0 ≠ 1 ∧ 𝐴𝐵 ) )
11 f1oprg ( ( ( 0 ∈ ℤ ∧ 𝐴𝑆 ) ∧ ( 1 ∈ ℤ ∧ 𝐵𝑆 ) ) → ( ( 0 ≠ 1 ∧ 𝐴𝐵 ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } : { 0 , 1 } –1-1-onto→ { 𝐴 , 𝐵 } ) )
12 7 10 11 sylc ( ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } : { 0 , 1 } –1-1-onto→ { 𝐴 , 𝐵 } )
13 eqcom ( 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ↔ ⟨“ 𝐴 𝐵 ”⟩ = 𝐸 )
14 s2prop ( ( 𝐴𝑆𝐵𝑆 ) → ⟨“ 𝐴 𝐵 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
15 14 3adant3 ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) → ⟨“ 𝐴 𝐵 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
16 15 eqeq1d ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) → ( ⟨“ 𝐴 𝐵 ”⟩ = 𝐸 ↔ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } = 𝐸 ) )
17 13 16 syl5bb ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) → ( 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ↔ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } = 𝐸 ) )
18 17 biimpa ( ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } = 𝐸 )
19 18 f1oeq1d ( ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } : { 0 , 1 } –1-1-onto→ { 𝐴 , 𝐵 } ↔ 𝐸 : { 0 , 1 } –1-1-onto→ { 𝐴 , 𝐵 } ) )
20 12 19 mpbid ( ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → 𝐸 : { 0 , 1 } –1-1-onto→ { 𝐴 , 𝐵 } )
21 20 ex ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) → ( 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ → 𝐸 : { 0 , 1 } –1-1-onto→ { 𝐴 , 𝐵 } ) )