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	$$⊢\phi \to I\in D$$
Assertion	s1f1	$$⊢\phi \to ⟨“I”⟩:\mathrm{dom}⟨“I”⟩\underset{1-1}{⟶}D$$

Proof

Step	Hyp	Ref	Expression
1		s1f1.1	$$⊢\phi \to I\in D$$
2		0nn0	$$⊢0\in {\mathbb{N}}_0$$
3	2	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
4		f1osng	$$⊢\left(0\in {\mathbb{N}}_0\wedge I\in D\right)\to \left\{⟨0,I⟩\right\}:\left\{0\right\}\underset{1-1\; onto}{⟶}\left\{I\right\}$$
5	3 1 4	syl2anc	$$⊢\phi \to \left\{⟨0,I⟩\right\}:\left\{0\right\}\underset{1-1\; onto}{⟶}\left\{I\right\}$$
6		f1of1	$$⊢\left\{⟨0,I⟩\right\}:\left\{0\right\}\underset{1-1\; onto}{⟶}\left\{I\right\}\to \left\{⟨0,I⟩\right\}:\left\{0\right\}\underset{1-1}{⟶}\left\{I\right\}$$
7	5 6	syl	$$⊢\phi \to \left\{⟨0,I⟩\right\}:\left\{0\right\}\underset{1-1}{⟶}\left\{I\right\}$$
8	1	snssd	$$⊢\phi \to \left\{I\right\}\subseteq D$$
9		f1ss	$$⊢\left(\left\{⟨0,I⟩\right\}:\left\{0\right\}\underset{1-1}{⟶}\left\{I\right\}\wedge \left\{I\right\}\subseteq D\right)\to \left\{⟨0,I⟩\right\}:\left\{0\right\}\underset{1-1}{⟶}D$$
10	7 8 9	syl2anc	$$⊢\phi \to \left\{⟨0,I⟩\right\}:\left\{0\right\}\underset{1-1}{⟶}D$$
11		s1val	$$⊢I\in D\to ⟨“I”⟩=\left\{⟨0,I⟩\right\}$$
12	1 11	syl	$$⊢\phi \to ⟨“I”⟩=\left\{⟨0,I⟩\right\}$$
13		s1dm	$$⊢\mathrm{dom}⟨“I”⟩=\left\{0\right\}$$
14	13	a1i	$$⊢\phi \to \mathrm{dom}⟨“I”⟩=\left\{0\right\}$$
15		eqidd	$$⊢\phi \to D=D$$
16	12 14 15	f1eq123d	$$⊢\phi \to \left(⟨“I”⟩:\mathrm{dom}⟨“I”⟩\underset{1-1}{⟶}D\leftrightarrow \left\{⟨0,I⟩\right\}:\left\{0\right\}\underset{1-1}{⟶}D\right)$$
17	10 16	mpbird	$$⊢\phi \to ⟨“I”⟩:\mathrm{dom}⟨“I”⟩\underset{1-1}{⟶}D$$