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 = { y | E. b e. B y = { <. S , b >. } }
	fsetsnf.f	|- F = ( x e. B |-> { <. S , x >. } )
Assertion	fsetsnf	|- ( S e. V -> F : B --> 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		simpr	|- ( ( S e. V /\ x e. B ) -> x e. B )
4		opeq2	|- ( b = x -> <. S , b >. = <. S , x >. )
5	4	sneqd	|- ( b = x -> { <. S , b >. } = { <. S , x >. } )
6	5	eqeq2d	|- ( b = x -> ( { <. S , x >. } = { <. S , b >. } <-> { <. S , x >. } = { <. S , x >. } ) )
7	6	adantl	|- ( ( ( S e. V /\ x e. B ) /\ b = x ) -> ( { <. S , x >. } = { <. S , b >. } <-> { <. S , x >. } = { <. S , x >. } ) )
8		eqidd	|- ( ( S e. V /\ x e. B ) -> { <. S , x >. } = { <. S , x >. } )
9	3 7 8	rspcedvd	|- ( ( S e. V /\ x e. B ) -> E. b e. B { <. S , x >. } = { <. S , b >. } )
10		snex	|- { <. S , x >. } e. _V
11		eqeq1	|- ( y = { <. S , x >. } -> ( y = { <. S , b >. } <-> { <. S , x >. } = { <. S , b >. } ) )
12	11	rexbidv	|- ( y = { <. S , x >. } -> ( E. b e. B y = { <. S , b >. } <-> E. b e. B { <. S , x >. } = { <. S , b >. } ) )
13	10 12 1	elab2	|- ( { <. S , x >. } e. A <-> E. b e. B { <. S , x >. } = { <. S , b >. } )
14	9 13	sylibr	|- ( ( S e. V /\ x e. B ) -> { <. S , x >. } e. A )
15	14 2	fmptd	|- ( S e. V -> F : B --> A )