mof0

Description: There is at most one function into the empty set. (Contributed by Zhi Wang, 19-Sep-2024)

		Ref	Expression
	Assertion	mof0	$⊢ \exists^{*} f f : A ⟶ \emptyset$

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		eqeq2	$⊢ g = \emptyset \to (f = g \leftrightarrow f = \emptyset)$
3	2	imbi2d	$⊢ g = \emptyset \to ((f : A ⟶ \emptyset \to f = g) \leftrightarrow (f : A ⟶ \emptyset \to f = \emptyset))$
4	3	albidv	$⊢ g = \emptyset \to (\forall f (f : A ⟶ \emptyset \to f = g) \leftrightarrow \forall f (f : A ⟶ \emptyset \to f = \emptyset))$
5	1 4	spcev	$⊢ \forall f (f : A ⟶ \emptyset \to f = \emptyset) \to \exists g \forall f (f : A ⟶ \emptyset \to f = g)$
6		f00	$⊢ f : A ⟶ \emptyset \leftrightarrow (f = \emptyset \land A = \emptyset)$
7	6	simplbi	$⊢ f : A ⟶ \emptyset \to f = \emptyset$
8	5 7	mpg	$⊢ \exists g \forall f (f : A ⟶ \emptyset \to f = g)$
9		df-mo	$⊢ \exists^{*} f f : A ⟶ \emptyset \leftrightarrow \exists g \forall f (f : A ⟶ \emptyset \to f = g)$
10	8 9	mpbir	$⊢ \exists^{*} f f : A ⟶ \emptyset$

Metamath Proof Explorer