Theorem fsetsnfo

Description: The mapping of an element of a class to a singleton function is a surjection. (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	fsetsnfo	$$⊢S\in V\to F:B\underset{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	fsetsnf	$$⊢S\in V\to F:B⟶A$$
4		vex	$$⊢m\in \mathrm{V}$$
5		eqeq1	$$⊢y=m\to \left(y=\left\{⟨S,b⟩\right\}\leftrightarrow m=\left\{⟨S,b⟩\right\}\right)$$
6	5	rexbidv	$$⊢y=m\to \left(\exists b\in By=\left\{⟨S,b⟩\right\}\leftrightarrow \exists b\in Bm=\left\{⟨S,b⟩\right\}\right)$$
7	4 6 1	elab2	$$⊢m\in A\leftrightarrow \exists b\in Bm=\left\{⟨S,b⟩\right\}$$
8		opeq2	$$⊢b=n\to ⟨S,b⟩=⟨S,n⟩$$
9	8	sneqd	$$⊢b=n\to \left\{⟨S,b⟩\right\}=\left\{⟨S,n⟩\right\}$$
10	9	eqeq2d	$$⊢b=n\to \left(m=\left\{⟨S,b⟩\right\}\leftrightarrow m=\left\{⟨S,n⟩\right\}\right)$$
11	10	cbvrexvw	$$⊢\exists b\in Bm=\left\{⟨S,b⟩\right\}\leftrightarrow \exists n\in Bm=\left\{⟨S,n⟩\right\}$$
12		simpr	$$⊢\left(\left(S\in V\wedge n\in B\right)\wedge m=\left\{⟨S,n⟩\right\}\right)\to m=\left\{⟨S,n⟩\right\}$$
13	2	a1i	$$⊢\left(S\in V\wedge n\in B\right)\to F=\left(x\in B⟼\left\{⟨S,x⟩\right\}\right)$$
14		opeq2	$$⊢x=n\to ⟨S,x⟩=⟨S,n⟩$$
15	14	sneqd	$$⊢x=n\to \left\{⟨S,x⟩\right\}=\left\{⟨S,n⟩\right\}$$
16	15	adantl	$$⊢\left(\left(S\in V\wedge n\in B\right)\wedge x=n\right)\to \left\{⟨S,x⟩\right\}=\left\{⟨S,n⟩\right\}$$
17		simpr	$$⊢\left(S\in V\wedge n\in B\right)\to n\in B$$
18		snex	$$⊢\left\{⟨S,n⟩\right\}\in \mathrm{V}$$
19	18	a1i	$$⊢\left(S\in V\wedge n\in B\right)\to \left\{⟨S,n⟩\right\}\in \mathrm{V}$$
20	13 16 17 19	fvmptd	$$⊢\left(S\in V\wedge n\in B\right)\to F\left(n\right)=\left\{⟨S,n⟩\right\}$$
21	20	eqcomd	$$⊢\left(S\in V\wedge n\in B\right)\to \left\{⟨S,n⟩\right\}=F\left(n\right)$$
22	21	adantr	$$⊢\left(\left(S\in V\wedge n\in B\right)\wedge m=\left\{⟨S,n⟩\right\}\right)\to \left\{⟨S,n⟩\right\}=F\left(n\right)$$
23	12 22	eqtrd	$$⊢\left(\left(S\in V\wedge n\in B\right)\wedge m=\left\{⟨S,n⟩\right\}\right)\to m=F\left(n\right)$$
24	23	ex	$$⊢\left(S\in V\wedge n\in B\right)\to \left(m=\left\{⟨S,n⟩\right\}\to m=F\left(n\right)\right)$$
25	24	reximdva	$$⊢S\in V\to \left(\exists n\in Bm=\left\{⟨S,n⟩\right\}\to \exists n\in Bm=F\left(n\right)\right)$$
26	11 25	syl5bi	$$⊢S\in V\to \left(\exists b\in Bm=\left\{⟨S,b⟩\right\}\to \exists n\in Bm=F\left(n\right)\right)$$
27	7 26	syl5bi	$$⊢S\in V\to \left(m\in A\to \exists n\in Bm=F\left(n\right)\right)$$
28	27	imp	$$⊢\left(S\in V\wedge m\in A\right)\to \exists n\in Bm=F\left(n\right)$$
29	28	ralrimiva	$$⊢S\in V\to \forall m\in A\exists n\in Bm=F\left(n\right)$$
30		dffo3	$$⊢F:B\underset{onto}{⟶}A\leftrightarrow \left(F:B⟶A\wedge \forall m\in A\exists n\in Bm=F\left(n\right)\right)$$
31	3 29 30	sylanbrc	$$⊢S\in V\to F:B\underset{onto}{⟶}A$$