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 = { y | E. b e. B y = { <. S , b >. } }
	fsetsnf.f	|- F = ( x e. B |-> { <. S , x >. } )
Assertion	fsetsnf1o	|- ( S e. V -> F : B -1-1-onto-> A )

Proof

Step	Hyp	Ref	Expression
1		fsetsnf.a	|- A = { y | E. b e. B y = { <. S , b >. } }
2		fsetsnf.f	|- F = ( x e. B |-> { <. S , x >. } )
3	1 2	fsetsnf1	|- ( S e. V -> F : B -1-1-> A )
4	1 2	fsetsnfo	|- ( S e. V -> F : B -onto-> A )
5		df-f1o	|- ( F : B -1-1-onto-> A <-> ( F : B -1-1-> A /\ F : B -onto-> A ) )
6	3 4 5	sylanbrc	|- ( S e. V -> F : B -1-1-onto-> A )