Theorem fsetsnf

Description: The mapping of an element of a class to a singleton function is a function. (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	fsetsnf	$$⊢S\in V\to F:B⟶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		simpr	$$⊢\left(S\in V\wedge x\in B\right)\to x\in B$$
4		opeq2	$$⊢b=x\to ⟨S,b⟩=⟨S,x⟩$$
5	4	sneqd	$$⊢b=x\to \left\{⟨S,b⟩\right\}=\left\{⟨S,x⟩\right\}$$
6	5	eqeq2d	$$⊢b=x\to \left(\left\{⟨S,x⟩\right\}=\left\{⟨S,b⟩\right\}\leftrightarrow \left\{⟨S,x⟩\right\}=\left\{⟨S,x⟩\right\}\right)$$
7	6	adantl	$$⊢\left(\left(S\in V\wedge x\in B\right)\wedge b=x\right)\to \left(\left\{⟨S,x⟩\right\}=\left\{⟨S,b⟩\right\}\leftrightarrow \left\{⟨S,x⟩\right\}=\left\{⟨S,x⟩\right\}\right)$$
8		eqidd	$$⊢\left(S\in V\wedge x\in B\right)\to \left\{⟨S,x⟩\right\}=\left\{⟨S,x⟩\right\}$$
9	3 7 8	rspcedvd	$$⊢\left(S\in V\wedge x\in B\right)\to \exists b\in B\left\{⟨S,x⟩\right\}=\left\{⟨S,b⟩\right\}$$
10		snex	$$⊢\left\{⟨S,x⟩\right\}\in \mathrm{V}$$
11		eqeq1	$$⊢y=\left\{⟨S,x⟩\right\}\to \left(y=\left\{⟨S,b⟩\right\}\leftrightarrow \left\{⟨S,x⟩\right\}=\left\{⟨S,b⟩\right\}\right)$$
12	11	rexbidv	$$⊢y=\left\{⟨S,x⟩\right\}\to \left(\exists b\in By=\left\{⟨S,b⟩\right\}\leftrightarrow \exists b\in B\left\{⟨S,x⟩\right\}=\left\{⟨S,b⟩\right\}\right)$$
13	10 12 1	elab2	$$⊢\left\{⟨S,x⟩\right\}\in A\leftrightarrow \exists b\in B\left\{⟨S,x⟩\right\}=\left\{⟨S,b⟩\right\}$$
14	9 13	sylibr	$$⊢\left(S\in V\wedge x\in B\right)\to \left\{⟨S,x⟩\right\}\in A$$
15	14 2	fmptd	$$⊢S\in V\to F:B⟶A$$