Theorem cfsetsnfsetfv

Description: The function value of the mapping of the class of singleton functions into the class of constant functions. (Contributed by AV, 13-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	cfsetsnfsetfv	|- ( ( A e. V /\ X e. G ) -> ( H ` X ) = ( a e. A |-> ( X ` Y ) ) )

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	3	a1i	|- ( ( A e. V /\ X e. G ) -> H = ( g e. G |-> ( a e. A |-> ( g ` Y ) ) ) )
5		fveq1	|- ( g = X -> ( g ` Y ) = ( X ` Y ) )
6	5	adantr	|- ( ( g = X /\ a e. A ) -> ( g ` Y ) = ( X ` Y ) )
7	6	mpteq2dva	|- ( g = X -> ( a e. A |-> ( g ` Y ) ) = ( a e. A |-> ( X ` Y ) ) )
8	7	adantl	|- ( ( ( A e. V /\ X e. G ) /\ g = X ) -> ( a e. A |-> ( g ` Y ) ) = ( a e. A |-> ( X ` Y ) ) )
9		simpr	|- ( ( A e. V /\ X e. G ) -> X e. G )
10		simpl	|- ( ( A e. V /\ X e. G ) -> A e. V )
11	10	mptexd	|- ( ( A e. V /\ X e. G ) -> ( a e. A |-> ( X ` Y ) ) e. _V )
12	4 8 9 11	fvmptd	|- ( ( A e. V /\ X e. G ) -> ( H ` X ) = ( a e. A |-> ( X ` Y ) ) )