Theorem cfsetsnfsetf1o

Description: The mapping of the class of singleton functions into the class of constant functions is a bijection. (Contributed by AV, 14-Sep-2024)

	Ref	Expression
Hypotheses	cfsetsnfsetfv.f	$$⊢F=\left\{f|\left(f:A⟶B\wedge \exists b\in B\forall z\in Af\left(z\right)=b\right)\right\}$$
	cfsetsnfsetfv.g	$$⊢G=\left\{x|x:\left\{Y\right\}⟶B\right\}$$
	cfsetsnfsetfv.h	$$⊢H=\left(g\in G⟼\left(a\in A⟼g\left(Y\right)\right)\right)$$
Assertion	cfsetsnfsetf1o	$$⊢\left(A\in V\wedge Y\in A\right)\to H:G\underset{1-1\; onto}{⟶}F$$

Proof

Step	Hyp	Ref	Expression
1		cfsetsnfsetfv.f	$$⊢F=\left\{f|\left(f:A⟶B\wedge \exists b\in B\forall z\in Af\left(z\right)=b\right)\right\}$$
2		cfsetsnfsetfv.g	$$⊢G=\left\{x|x:\left\{Y\right\}⟶B\right\}$$
3		cfsetsnfsetfv.h	$$⊢H=\left(g\in G⟼\left(a\in A⟼g\left(Y\right)\right)\right)$$
4	1 2 3	cfsetsnfsetf1	$$⊢\left(A\in V\wedge Y\in A\right)\to H:G\underset{1-1}{⟶}F$$
5	1 2 3	cfsetsnfsetfo	$$⊢\left(A\in V\wedge Y\in A\right)\to H:G\underset{onto}{⟶}F$$
6		df-f1o	$$⊢H:G\underset{1-1\; onto}{⟶}F\leftrightarrow \left(H:G\underset{1-1}{⟶}F\wedge H:G\underset{onto}{⟶}F\right)$$
7	4 5 6	sylanbrc	$$⊢\left(A\in V\wedge Y\in A\right)\to H:G\underset{1-1\; onto}{⟶}F$$