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