f1mo

Description: A function that maps a set with at most one element to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024)

		Ref	Expression
	Assertion	f1mo	$⊢ (\exists^{*} x x \in A \land F : A ⟶ B) \to F : A \underset{1-1}{⟶} B$

Step	Hyp	Ref	Expression
1		mo0sn	$⊢ \exists^{*} x x \in A \leftrightarrow (A = \emptyset \lor \exists y A = \{y\})$
2		f102g	$⊢ (A = \emptyset \land F : A ⟶ B) \to F : A \underset{1-1}{⟶} B$
3		vex	$⊢ y \in V$
4		f1sn2g	$⊢ (y \in V \land F : \{y\} ⟶ B) \to F : \{y\} \underset{1-1}{⟶} B$
5	3 4	mpan	$⊢ F : \{y\} ⟶ B \to F : \{y\} \underset{1-1}{⟶} B$
6		feq2	$⊢ A = \{y\} \to (F : A ⟶ B \leftrightarrow F : \{y\} ⟶ B)$
7		f1eq2	$⊢ A = \{y\} \to (F : A \underset{1-1}{⟶} B \leftrightarrow F : \{y\} \underset{1-1}{⟶} B)$
8	6 7	imbi12d	$⊢ A = \{y\} \to ((F : A ⟶ B \to F : A \underset{1-1}{⟶} B) \leftrightarrow (F : \{y\} ⟶ B \to F : \{y\} \underset{1-1}{⟶} B))$
9	5 8	mpbiri	$⊢ A = \{y\} \to (F : A ⟶ B \to F : A \underset{1-1}{⟶} B)$
10	9	exlimiv	$⊢ \exists y A = \{y\} \to (F : A ⟶ B \to F : A \underset{1-1}{⟶} B)$
11	10	imp	$⊢ (\exists y A = \{y\} \land F : A ⟶ B) \to F : A \underset{1-1}{⟶} B$
12	2 11	jaoian	$⊢ ((A = \emptyset \lor \exists y A = \{y\}) \land F : A ⟶ B) \to F : A \underset{1-1}{⟶} B$
13	1 12	sylanb	$⊢ (\exists^{*} x x \in A \land F : A ⟶ B) \to F : A \underset{1-1}{⟶} B$

Metamath Proof Explorer