Metamath Proof Explorer


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 b B z A f z = b
cfsetsnfsetfv.g G = x | x : Y B
cfsetsnfsetfv.h H = g G a A g Y
Assertion cfsetsnfsetfv A V X G H X = a A X Y

Proof

Step Hyp Ref Expression
1 cfsetsnfsetfv.f F = f | f : A B b B z A f z = b
2 cfsetsnfsetfv.g G = x | x : Y B
3 cfsetsnfsetfv.h H = g G a A g Y
4 3 a1i A V X G H = g G a A g Y
5 fveq1 g = X g Y = X Y
6 5 adantr g = X a A g Y = X Y
7 6 mpteq2dva g = X a A g Y = a A X Y
8 7 adantl A V X G g = X a A g Y = a A X Y
9 simpr A V X G X G
10 simpl A V X G A V
11 10 mptexd A V X G a A X Y V
12 4 8 9 11 fvmptd A V X G H X = a A X Y