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

Metamath Proof Explorer

Theorem s1f1

Description: Conditions for a length 1 string to be a one-to-one function. (Contributed by Thierry Arnoux, 11-Dec-2023)

Ref Expression
Hypothesis s1f1.1 ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
Assertion s1f1 ( 𝜑 → ⟨“ 𝐼 ”⟩ : dom ⟨“ 𝐼 ”⟩ –1-1→ 𝐷 )

Proof

Step Hyp Ref Expression
1 s1f1.1 ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
2 0nn0 ⊢ 0 ∈ ℕ0
3 2 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
4 f1osng ⊢ ( ( 0 ∈ ℕ0 ∧ 𝐼 ∈ 𝐷 ) → { ⟨ 0 , 𝐼 ⟩ } : { 0 } –1-1-onto→ { 𝐼 } )
5 3 1 4 syl2anc ⊢ ( 𝜑 → { ⟨ 0 , 𝐼 ⟩ } : { 0 } –1-1-onto→ { 𝐼 } )
6 f1of1 ⊢ ( { ⟨ 0 , 𝐼 ⟩ } : { 0 } –1-1-onto→ { 𝐼 } → { ⟨ 0 , 𝐼 ⟩ } : { 0 } –1-1→ { 𝐼 } )
7 5 6 syl ⊢ ( 𝜑 → { ⟨ 0 , 𝐼 ⟩ } : { 0 } –1-1→ { 𝐼 } )
8 1 snssd ⊢ ( 𝜑 → { 𝐼 } ⊆ 𝐷 )
9 f1ss ⊢ ( ( { ⟨ 0 , 𝐼 ⟩ } : { 0 } –1-1→ { 𝐼 } ∧ { 𝐼 } ⊆ 𝐷 ) → { ⟨ 0 , 𝐼 ⟩ } : { 0 } –1-1→ 𝐷 )
10 7 8 9 syl2anc ⊢ ( 𝜑 → { ⟨ 0 , 𝐼 ⟩ } : { 0 } –1-1→ 𝐷 )
11 s1val ⊢ ( 𝐼 ∈ 𝐷 → ⟨“ 𝐼 ”⟩ = { ⟨ 0 , 𝐼 ⟩ } )
12 1 11 syl ⊢ ( 𝜑 → ⟨“ 𝐼 ”⟩ = { ⟨ 0 , 𝐼 ⟩ } )
13 s1dm ⊢ dom ⟨“ 𝐼 ”⟩ = { 0 }
14 13 a1i ⊢ ( 𝜑 → dom ⟨“ 𝐼 ”⟩ = { 0 } )
15 eqidd ⊢ ( 𝜑 → 𝐷 = 𝐷 )
16 12 14 15 f1eq123d ⊢ ( 𝜑 → ( ⟨“ 𝐼 ”⟩ : dom ⟨“ 𝐼 ”⟩ –1-1→ 𝐷 ↔ { ⟨ 0 , 𝐼 ⟩ } : { 0 } –1-1→ 𝐷 ) )
17 10 16 mpbird ⊢ ( 𝜑 → ⟨“ 𝐼 ”⟩ : dom ⟨“ 𝐼 ”⟩ –1-1→ 𝐷 )