f102g

Description: A function that maps the empty set to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024)

		Ref	Expression
	Assertion	f102g	$⊢ (A = \emptyset \land F : A ⟶ B) \to F : A \underset{1-1}{⟶} B$

Step	Hyp	Ref	Expression
1		feq2	$⊢ A = \emptyset \to (F : A ⟶ B \leftrightarrow F : \emptyset ⟶ B)$
2	1	biimpa	$⊢ (A = \emptyset \land F : A ⟶ B) \to F : \emptyset ⟶ B$
3		f0bi	$⊢ F : \emptyset ⟶ B \leftrightarrow F = \emptyset$
4		f10	$⊢ \emptyset : \emptyset \underset{1-1}{⟶} B$
5		f1eq1	$⊢ F = \emptyset \to (F : \emptyset \underset{1-1}{⟶} B \leftrightarrow \emptyset : \emptyset \underset{1-1}{⟶} B)$
6	4 5	mpbiri	$⊢ F = \emptyset \to F : \emptyset \underset{1-1}{⟶} B$
7	3 6	sylbi	$⊢ F : \emptyset ⟶ B \to F : \emptyset \underset{1-1}{⟶} B$
8	2 7	syl	$⊢ (A = \emptyset \land F : A ⟶ B) \to F : \emptyset \underset{1-1}{⟶} B$
9		f1eq2	$⊢ A = \emptyset \to (F : A \underset{1-1}{⟶} B \leftrightarrow F : \emptyset \underset{1-1}{⟶} B)$
10	9	adantr	$⊢ (A = \emptyset \land F : A ⟶ B) \to (F : A \underset{1-1}{⟶} B \leftrightarrow F : \emptyset \underset{1-1}{⟶} B)$
11	8 10	mpbird	$⊢ (A = \emptyset \land F : A ⟶ B) \to F : A \underset{1-1}{⟶} B$

Metamath Proof Explorer