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𝐷 )