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=\left\{Y\right\}\to {\exists }^{*}ff:A⟶B$$

Proof

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