Theorem f1cdmsn

Description: If a one-to-one function with a nonempty domain has a singleton as its codomain, its domain must also be a singleton. (Contributed by BTernaryTau, 1-Dec-2024)

	Ref	Expression
Assertion	f1cdmsn	$$⊢\left(F:A\underset{1-1}{⟶}\left\{B\right\}\wedge A\ne \varnothing \right)\to \exists xA=\left\{x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		f1f	$$⊢F:A\underset{1-1}{⟶}\left\{B\right\}\to F:A⟶\left\{B\right\}$$
2		fvconst	$$⊢\left(F:A⟶\left\{B\right\}\wedge y\in A\right)\to F\left(y\right)=B$$
3	2	3adant3	$$⊢\left(F:A⟶\left\{B\right\}\wedge y\in A\wedge z\in A\right)\to F\left(y\right)=B$$
4		fvconst	$$⊢\left(F:A⟶\left\{B\right\}\wedge z\in A\right)\to F\left(z\right)=B$$
5	4	3adant2	$$⊢\left(F:A⟶\left\{B\right\}\wedge y\in A\wedge z\in A\right)\to F\left(z\right)=B$$
6	3 5	eqtr4d	$$⊢\left(F:A⟶\left\{B\right\}\wedge y\in A\wedge z\in A\right)\to F\left(y\right)=F\left(z\right)$$
7	1 6	syl3an1	$$⊢\left(F:A\underset{1-1}{⟶}\left\{B\right\}\wedge y\in A\wedge z\in A\right)\to F\left(y\right)=F\left(z\right)$$
8		f1veqaeq	$$⊢\left(F:A\underset{1-1}{⟶}\left\{B\right\}\wedge \left(y\in A\wedge z\in A\right)\right)\to \left(F\left(y\right)=F\left(z\right)\to y=z\right)$$
9	8	3impb	$$⊢\left(F:A\underset{1-1}{⟶}\left\{B\right\}\wedge y\in A\wedge z\in A\right)\to \left(F\left(y\right)=F\left(z\right)\to y=z\right)$$
10	7 9	mpd	$$⊢\left(F:A\underset{1-1}{⟶}\left\{B\right\}\wedge y\in A\wedge z\in A\right)\to y=z$$
11	10	3expia	$$⊢\left(F:A\underset{1-1}{⟶}\left\{B\right\}\wedge y\in A\right)\to \left(z\in A\to y=z\right)$$
12	11	ralrimiv	$$⊢\left(F:A\underset{1-1}{⟶}\left\{B\right\}\wedge y\in A\right)\to \forall z\in Ay=z$$
13	12	reximdva0	$$⊢\left(F:A\underset{1-1}{⟶}\left\{B\right\}\wedge A\ne \varnothing \right)\to \exists y\in A\forall z\in Ay=z$$
14		issn	$$⊢\exists y\in A\forall z\in Ay=z\to \exists xA=\left\{x\right\}$$
15	13 14	syl	$$⊢\left(F:A\underset{1-1}{⟶}\left\{B\right\}\wedge A\ne \varnothing \right)\to \exists xA=\left\{x\right\}$$