This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem s111

Description: The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s111 ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( ⟨“ 𝑆 ”⟩ = ⟨“ 𝑇 ”⟩ ↔ 𝑆 = 𝑇 ) )

Proof

Step Hyp Ref Expression
1 s1val ⊢ ( 𝑆 ∈ 𝐴 → ⟨“ 𝑆 ”⟩ = { ⟨ 0 , 𝑆 ⟩ } )
2 s1val ⊢ ( 𝑇 ∈ 𝐴 → ⟨“ 𝑇 ”⟩ = { ⟨ 0 , 𝑇 ⟩ } )
3 1 2 eqeqan12d ⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( ⟨“ 𝑆 ”⟩ = ⟨“ 𝑇 ”⟩ ↔ { ⟨ 0 , 𝑆 ⟩ } = { ⟨ 0 , 𝑇 ⟩ } ) )
4 opex ⊢ ⟨ 0 , 𝑆 ⟩ ∈ V
5 sneqbg ⊢ ( ⟨ 0 , 𝑆 ⟩ ∈ V → ( { ⟨ 0 , 𝑆 ⟩ } = { ⟨ 0 , 𝑇 ⟩ } ↔ ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ) )
6 4 5 mp1i ⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( { ⟨ 0 , 𝑆 ⟩ } = { ⟨ 0 , 𝑇 ⟩ } ↔ ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ) )
7 0z ⊢ 0 ∈ ℤ
8 eqid ⊢ 0 = 0
9 opthg ⊢ ( ( 0 ∈ ℤ ∧ 𝑆 ∈ 𝐴 ) → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ ( 0 = 0 ∧ 𝑆 = 𝑇 ) ) )
10 9 baibd ⊢ ( ( ( 0 ∈ ℤ ∧ 𝑆 ∈ 𝐴 ) ∧ 0 = 0 ) → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ 𝑆 = 𝑇 ) )
11 8 10 mpan2 ⊢ ( ( 0 ∈ ℤ ∧ 𝑆 ∈ 𝐴 ) → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ 𝑆 = 𝑇 ) )
12 7 11 mpan ⊢ ( 𝑆 ∈ 𝐴 → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ 𝑆 = 𝑇 ) )
13 12 adantr ⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 0 , 𝑇 ⟩ ↔ 𝑆 = 𝑇 ) )
14 3 6 13 3bitrd ⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( ⟨“ 𝑆 ”⟩ = ⟨“ 𝑇 ”⟩ ↔ 𝑆 = 𝑇 ) )