Theorem fsetsnf1o

Description: The mapping of an element of a class to a singleton function is a bijection. (Contributed by AV, 13-Sep-2024)

	Ref	Expression
Hypotheses	fsetsnf.a	$$⊢A=\left\{y|\exists b\in By=\left\{⟨S,b⟩\right\}\right\}$$
	fsetsnf.f	$$⊢F=\left(x\in B⟼\left\{⟨S,x⟩\right\}\right)$$
Assertion	fsetsnf1o	$$⊢S\in V\to F:B\underset{1-1\; onto}{⟶}A$$

Proof

Step	Hyp	Ref	Expression
1		fsetsnf.a	$$⊢A=\left\{y|\exists b\in By=\left\{⟨S,b⟩\right\}\right\}$$
2		fsetsnf.f	$$⊢F=\left(x\in B⟼\left\{⟨S,x⟩\right\}\right)$$
3	1 2	fsetsnf1	$$⊢S\in V\to F:B\underset{1-1}{⟶}A$$
4	1 2	fsetsnfo	$$⊢S\in V\to F:B\underset{onto}{⟶}A$$
5		df-f1o	$$⊢F:B\underset{1-1\; onto}{⟶}A\leftrightarrow \left(F:B\underset{1-1}{⟶}A\wedge F:B\underset{onto}{⟶}A\right)$$
6	3 4 5	sylanbrc	$$⊢S\in V\to F:B\underset{1-1\; onto}{⟶}A$$