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 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → { 0 , 1 } = { 0 , 1 } )
20 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → { 𝐴 , 𝐵 } = { 𝐴 , 𝐵 } )
21 18 19 20 f1oeq123d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } : { 0 , 1 } –1-1-onto→ { 𝐴 , 𝐵 } ↔ 𝐸 : { 0 , 1 } –1-1-onto→ { 𝐴 , 𝐵 } ) )
22 12 21 mpbid ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ ) → 𝐸 : { 0 , 1 } –1-1-onto→ { 𝐴 , 𝐵 } )
23 22 ex ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐸 = ⟨“ 𝐴 𝐵 ”⟩ → 𝐸 : { 0 , 1 } –1-1-onto→ { 𝐴 , 𝐵 } ) )