cfsetsnfsetf

Description: The mapping of the class of singleton functions into the class of constant functions is a function. (Contributed by AV, 14-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	cfsetsnfsetf	$⊢ (A \in V \land Y \in A) \to H : G ⟶ F$

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		simpl	$⊢ (A \in V \land Y \in A) \to A \in V$
5	4	adantr	$⊢ ((A \in V \land Y \in A) \land g \in G) \to A \in V$
6	5	mptexd	$⊢ ((A \in V \land Y \in A) \land g \in G) \to (a \in A ⟼ g (Y)) \in V$
7		vex	$⊢ g \in V$
8		feq1	$⊢ x = g \to (x : \{Y\} ⟶ B \leftrightarrow g : \{Y\} ⟶ B)$
9	7 8 2	elab2	$⊢ g \in G \leftrightarrow g : \{Y\} ⟶ B$
10	9	biimpi	$⊢ g \in G \to g : \{Y\} ⟶ B$
11	10	adantl	$⊢ ((A \in V \land Y \in A) \land g \in G) \to g : \{Y\} ⟶ B$
12		snidg	$⊢ Y \in A \to Y \in \{Y\}$
13	12	adantl	$⊢ (A \in V \land Y \in A) \to Y \in \{Y\}$
14	13	adantr	$⊢ ((A \in V \land Y \in A) \land g \in G) \to Y \in \{Y\}$
15	11 14	ffvelrnd	$⊢ ((A \in V \land Y \in A) \land g \in G) \to g (Y) \in B$
16	15	adantr	$⊢ (((A \in V \land Y \in A) \land g \in G) \land a \in A) \to g (Y) \in B$
17	16	fmpttd	$⊢ ((A \in V \land Y \in A) \land g \in G) \to (a \in A ⟼ g (Y)) : A ⟶ B$
18		eqeq2	$⊢ b = g (Y) \to (g (Y) = b \leftrightarrow g (Y) = g (Y))$
19	18	ralbidv	$⊢ b = g (Y) \to (\forall z \in A g (Y) = b \leftrightarrow \forall z \in A g (Y) = g (Y))$
20	19	adantl	$⊢ (((A \in V \land Y \in A) \land g \in G) \land b = g (Y)) \to (\forall z \in A g (Y) = b \leftrightarrow \forall z \in A g (Y) = g (Y))$
21		eqidd	$⊢ (((A \in V \land Y \in A) \land g \in G) \land z \in A) \to g (Y) = g (Y)$
22	21	ralrimiva	$⊢ ((A \in V \land Y \in A) \land g \in G) \to \forall z \in A g (Y) = g (Y)$
23	15 20 22	rspcedvd	$⊢ ((A \in V \land Y \in A) \land g \in G) \to \exists b \in B \forall z \in A g (Y) = b$
24	17 23	jca	$⊢ ((A \in V \land Y \in A) \land g \in G) \to ((a \in A ⟼ g (Y)) : A ⟶ B \land \exists b \in B \forall z \in A g (Y) = b)$
25		feq1	$⊢ f = (a \in A ⟼ g (Y)) \to (f : A ⟶ B \leftrightarrow (a \in A ⟼ g (Y)) : A ⟶ B)$
26		simpl	$⊢ (f = (a \in A ⟼ g (Y)) \land z \in A) \to f = (a \in A ⟼ g (Y))$
27		eqidd	$⊢ ((f = (a \in A ⟼ g (Y)) \land z \in A) \land a = z) \to g (Y) = g (Y)$
28		simpr	$⊢ (f = (a \in A ⟼ g (Y)) \land z \in A) \to z \in A$
29		fvexd	$⊢ (f = (a \in A ⟼ g (Y)) \land z \in A) \to g (Y) \in V$
30		nfcv	$⊢ \underline{Ⅎ} a f$
31		nfmpt1	$⊢ \underline{Ⅎ} a (a \in A ⟼ g (Y))$
32	30 31	nfeq	$⊢ Ⅎ a f = (a \in A ⟼ g (Y))$
33		nfv	$⊢ Ⅎ a z \in A$
34	32 33	nfan	$⊢ Ⅎ a (f = (a \in A ⟼ g (Y)) \land z \in A)$
35		nfcv	$⊢ \underline{Ⅎ} a z$
36		nfcv	$⊢ \underline{Ⅎ} a g (Y)$
37	26 27 28 29 34 35 36	fvmptdf	$⊢ (f = (a \in A ⟼ g (Y)) \land z \in A) \to f (z) = g (Y)$
38	37	eqeq1d	$⊢ (f = (a \in A ⟼ g (Y)) \land z \in A) \to (f (z) = b \leftrightarrow g (Y) = b)$
39	38	ralbidva	$⊢ f = (a \in A ⟼ g (Y)) \to (\forall z \in A f (z) = b \leftrightarrow \forall z \in A g (Y) = b)$
40	39	rexbidv	$⊢ f = (a \in A ⟼ g (Y)) \to (\exists b \in B \forall z \in A f (z) = b \leftrightarrow \exists b \in B \forall z \in A g (Y) = b)$
41	25 40	anbi12d	$⊢ f = (a \in A ⟼ g (Y)) \to ((f : A ⟶ B \land \exists b \in B \forall z \in A f (z) = b) \leftrightarrow ((a \in A ⟼ g (Y)) : A ⟶ B \land \exists b \in B \forall z \in A g (Y) = b))$
42	6 24 41	elabd	$⊢ ((A \in V \land Y \in A) \land g \in G) \to (a \in A ⟼ g (Y)) \in \{f \| (f : A ⟶ B \land \exists b \in B \forall z \in A f (z) = b)\}$
43	42 1	eleqtrrdi	$⊢ ((A \in V \land Y \in A) \land g \in G) \to (a \in A ⟼ g (Y)) \in F$
44	43 3	fmptd	$⊢ (A \in V \land Y \in A) \to H : G ⟶ F$

Metamath Proof Explorer

Theorem cfsetsnfsetf

Proof