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

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

Metamath Proof Explorer