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 \land \exists b \in B \forall z \in A f (z) = b)\}$
		cfsetsnfsetfv.g	$⊢ G = \{x \| x : \{Y\} ⟶ B\}$
		cfsetsnfsetfv.h	$⊢ H = (g \in G ⟼ (a \in A ⟼ g (Y)))$
	Assertion	cfsetsnfsetfv	$⊢ (A \in V \land X \in G) \to H (X) = (a \in A ⟼ X (Y))$

Proof

Step	Hyp	Ref	Expression
1		cfsetsnfsetfv.f	$⊢ F = \{f \| (f : A ⟶ B \land \exists b \in B \forall z \in A f (z) = b)\}$
2		cfsetsnfsetfv.g	$⊢ G = \{x \| x : \{Y\} ⟶ B\}$
3		cfsetsnfsetfv.h	$⊢ H = (g \in G ⟼ (a \in A ⟼ g (Y)))$
4	3	a1i	$⊢ (A \in V \land X \in G) \to H = (g \in G ⟼ (a \in A ⟼ g (Y)))$
5		fveq1	$⊢ g = X \to g (Y) = X (Y)$
6	5	adantr	$⊢ (g = X \land a \in A) \to g (Y) = X (Y)$
7	6	mpteq2dva	$⊢ g = X \to (a \in A ⟼ g (Y)) = (a \in A ⟼ X (Y))$
8	7	adantl	$⊢ ((A \in V \land X \in G) \land g = X) \to (a \in A ⟼ g (Y)) = (a \in A ⟼ X (Y))$
9		simpr	$⊢ (A \in V \land X \in G) \to X \in G$
10		simpl	$⊢ (A \in V \land X \in G) \to A \in V$
11	10	mptexd	$⊢ (A \in V \land X \in G) \to (a \in A ⟼ X (Y)) \in V$
12	4 8 9 11	fvmptd	$⊢ (A \in V \land X \in G) \to H (X) = (a \in A ⟼ X (Y))$