Theorem 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	$$⊢\left({\exists }^{*}xx\in A\wedge F:A⟶B\right)\to F:A\underset{1-1}{⟶}B$$

Proof

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