This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mofsn2

Description: There is at most one function into a singleton. An unconditional variant of mofsn , i.e., the singleton could be empty if Y is a proper class. (Contributed by Zhi Wang, 19-Sep-2024)

		Ref	Expression
	Assertion	mofsn2	$⊢ B = \{Y\} \to \exists^{*} f f : A ⟶ B$

Proof

Step	Hyp	Ref	Expression
1		mofsn	$⊢ Y \in V \to \exists^{*} f f : A ⟶ \{Y\}$
2	1	adantl	$⊢ (B = \{Y\} \land Y \in V) \to \exists^{*} f f : A ⟶ \{Y\}$
3		feq3	$⊢ B = \{Y\} \to (f : A ⟶ B \leftrightarrow f : A ⟶ \{Y\})$
4	3	mobidv	$⊢ B = \{Y\} \to (\exists^{} f f : A ⟶ B \leftrightarrow \exists^{} f f : A ⟶ \{Y\})$
5	4	adantr	$⊢ (B = \{Y\} \land Y \in V) \to (\exists^{} f f : A ⟶ B \leftrightarrow \exists^{} f f : A ⟶ \{Y\})$
6	2 5	mpbird	$⊢ (B = \{Y\} \land Y \in V) \to \exists^{*} f f : A ⟶ B$
7		simpl	$⊢ (B = \{Y\} \land \neg Y \in V) \to B = \{Y\}$
8		snprc	$⊢ \neg Y \in V \leftrightarrow \{Y\} = \emptyset$
9	8	biimpi	$⊢ \neg Y \in V \to \{Y\} = \emptyset$
10	9	adantl	$⊢ (B = \{Y\} \land \neg Y \in V) \to \{Y\} = \emptyset$
11	7 10	eqtrd	$⊢ (B = \{Y\} \land \neg Y \in V) \to B = \emptyset$
12		mof02	$⊢ B = \emptyset \to \exists^{*} f f : A ⟶ B$
13	11 12	syl	$⊢ (B = \{Y\} \land \neg Y \in V) \to \exists^{*} f f : A ⟶ B$
14	6 13	pm2.61dan	$⊢ B = \{Y\} \to \exists^{*} f f : A ⟶ B$