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

Metamath Proof Explorer

Theorem cfsetsnfsetf

Proof