Theorem cfsetsnfsetf1o

Description: The mapping of the class of singleton functions into the class of constant functions is a bijection. (Contributed by AV, 14-Sep-2024)

	Ref	Expression
Hypotheses	cfsetsnfsetfv.f	|- F = { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) }
	cfsetsnfsetfv.g	|- G = { x | x : { Y } --> B }
	cfsetsnfsetfv.h	|- H = ( g e. G |-> ( a e. A |-> ( g ` Y ) ) )
Assertion	cfsetsnfsetf1o	|- ( ( A e. V /\ Y e. A ) -> H : G -1-1-onto-> F )

Proof

Step	Hyp	Ref	Expression
1		cfsetsnfsetfv.f	|- F = { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) }
2		cfsetsnfsetfv.g	|- G = { x | x : { Y } --> B }
3		cfsetsnfsetfv.h	|- H = ( g e. G |-> ( a e. A |-> ( g ` Y ) ) )
4	1 2 3	cfsetsnfsetf1	|- ( ( A e. V /\ Y e. A ) -> H : G -1-1-> F )
5	1 2 3	cfsetsnfsetfo	|- ( ( A e. V /\ Y e. A ) -> H : G -onto-> F )
6		df-f1o	|- ( H : G -1-1-onto-> F <-> ( H : G -1-1-> F /\ H : G -onto-> F ) )
7	4 5 6	sylanbrc	|- ( ( A e. V /\ Y e. A ) -> H : G -1-1-onto-> F )