cfsetsnfsetfo

Description: The mapping of the class of singleton functions into the class of constant functions is a surjection. (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	cfsetsnfsetfo	$⊢ (A \in V \land Y \in A) \to H : G \underset{onto}{⟶} 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	1 2 3	cfsetsnfsetf	$⊢ (A \in V \land Y \in A) \to H : G ⟶ F$
5		vex	$⊢ m \in V$
6		feq1	$⊢ f = m \to (f : A ⟶ B \leftrightarrow m : A ⟶ B)$
7		fveq1	$⊢ f = m \to f (z) = m (z)$
8	7	adantr	$⊢ (f = m \land z \in A) \to f (z) = m (z)$
9	8	eqeq1d	$⊢ (f = m \land z \in A) \to (f (z) = b \leftrightarrow m (z) = b)$
10	9	ralbidva	$⊢ f = m \to (\forall z \in A f (z) = b \leftrightarrow \forall z \in A m (z) = b)$
11	10	rexbidv	$⊢ f = m \to (\exists b \in B \forall z \in A f (z) = b \leftrightarrow \exists b \in B \forall z \in A m (z) = b)$
12	6 11	anbi12d	$⊢ f = m \to ((f : A ⟶ B \land \exists b \in B \forall z \in A f (z) = b) \leftrightarrow (m : A ⟶ B \land \exists b \in B \forall z \in A m (z) = b))$
13	5 12 1	elab2	$⊢ m \in F \leftrightarrow (m : A ⟶ B \land \exists b \in B \forall z \in A m (z) = b)$
14		simpllr	$⊢ (((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land \forall z \in A m (z) = b) \land y \in \{Y\}) \to b \in B$
15		eqid	$⊢ (y \in \{Y\} ⟼ b) = (y \in \{Y\} ⟼ b)$
16	14 15	fmptd	$⊢ ((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land \forall z \in A m (z) = b) \to (y \in \{Y\} ⟼ b) : \{Y\} ⟶ B$
17		snex	$⊢ \{Y\} \in V$
18	17	mptex	$⊢ (y \in \{Y\} ⟼ b) \in V$
19		feq1	$⊢ x = (y \in \{Y\} ⟼ b) \to (x : \{Y\} ⟶ B \leftrightarrow (y \in \{Y\} ⟼ b) : \{Y\} ⟶ B)$
20	18 19 2	elab2	$⊢ (y \in \{Y\} ⟼ b) \in G \leftrightarrow (y \in \{Y\} ⟼ b) : \{Y\} ⟶ B$
21	16 20	sylibr	$⊢ ((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land \forall z \in A m (z) = b) \to (y \in \{Y\} ⟼ b) \in G$
22		fveq1	$⊢ n = (y \in \{Y\} ⟼ b) \to n (Y) = (y \in \{Y\} ⟼ b) (Y)$
23	22	mpteq2dv	$⊢ n = (y \in \{Y\} ⟼ b) \to (a \in A ⟼ n (Y)) = (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y))$
24	23	eqeq2d	$⊢ n = (y \in \{Y\} ⟼ b) \to (m = (a \in A ⟼ n (Y)) \leftrightarrow m = (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)))$
25	24	adantl	$⊢ (((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land \forall z \in A m (z) = b) \land n = (y \in \{Y\} ⟼ b)) \to (m = (a \in A ⟼ n (Y)) \leftrightarrow m = (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)))$
26		simpr	$⊢ (((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land z \in A) \land m (z) = b) \to m (z) = b$
27		eqidd	$⊢ (((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land z \in A) \land m (z) = b) \to (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) = (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y))$
28		eqidd	$⊢ ((((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land z \in A) \land m (z) = b) \land a = z) \to (y \in \{Y\} ⟼ b) = (y \in \{Y\} ⟼ b)$
29		eqidd	$⊢ (((((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land z \in A) \land m (z) = b) \land a = z) \land y = Y) \to b = b$
30		snidg	$⊢ Y \in A \to Y \in \{Y\}$
31	30	ad6antlr	$⊢ ((((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land z \in A) \land m (z) = b) \land a = z) \to Y \in \{Y\}$
32		simpllr	$⊢ (((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land z \in A) \land m (z) = b) \to b \in B$
33	32	adantr	$⊢ ((((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land z \in A) \land m (z) = b) \land a = z) \to b \in B$
34	28 29 31 33	fvmptd	$⊢ ((((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land z \in A) \land m (z) = b) \land a = z) \to (y \in \{Y\} ⟼ b) (Y) = b$
35		simpr	$⊢ ((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land z \in A) \to z \in A$
36	35	adantr	$⊢ (((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land z \in A) \land m (z) = b) \to z \in A$
37	27 34 36 32	fvmptd	$⊢ (((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land z \in A) \land m (z) = b) \to (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) (z) = b$
38	26 37	eqtr4d	$⊢ (((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land z \in A) \land m (z) = b) \to m (z) = (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) (z)$
39	38	ex	$⊢ ((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land z \in A) \to (m (z) = b \to m (z) = (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) (z))$
40	39	ralimdva	$⊢ (((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \to (\forall z \in A m (z) = b \to \forall z \in A m (z) = (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) (z))$
41	40	imp	$⊢ ((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land \forall z \in A m (z) = b) \to \forall z \in A m (z) = (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) (z)$
42		ffn	$⊢ m : A ⟶ B \to m Fn A$
43	42	adantl	$⊢ ((A \in V \land Y \in A) \land m : A ⟶ B) \to m Fn A$
44		nfv	$⊢ Ⅎ a ((A \in V \land Y \in A) \land m : A ⟶ B)$
45		fvexd	$⊢ (((A \in V \land Y \in A) \land m : A ⟶ B) \land a \in A) \to (y \in \{Y\} ⟼ b) (Y) \in V$
46		eqid	$⊢ (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) = (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y))$
47	44 45 46	fnmptd	$⊢ ((A \in V \land Y \in A) \land m : A ⟶ B) \to (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) Fn A$
48	43 47	jca	$⊢ ((A \in V \land Y \in A) \land m : A ⟶ B) \to (m Fn A \land (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) Fn A)$
49	48	adantr	$⊢ (((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \to (m Fn A \land (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) Fn A)$
50	49	adantr	$⊢ ((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land \forall z \in A m (z) = b) \to (m Fn A \land (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) Fn A)$
51		eqfnfv	$⊢ (m Fn A \land (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) Fn A) \to (m = (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) \leftrightarrow \forall z \in A m (z) = (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) (z))$
52	50 51	syl	$⊢ ((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land \forall z \in A m (z) = b) \to (m = (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) \leftrightarrow \forall z \in A m (z) = (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y)) (z))$
53	41 52	mpbird	$⊢ ((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land \forall z \in A m (z) = b) \to m = (a \in A ⟼ (y \in \{Y\} ⟼ b) (Y))$
54	21 25 53	rspcedvd	$⊢ ((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land \forall z \in A m (z) = b) \to \exists n \in G m = (a \in A ⟼ n (Y))$
55		simp-4l	$⊢ ((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land \forall z \in A m (z) = b) \to A \in V$
56	1 2 3	cfsetsnfsetfv	$⊢ (A \in V \land n \in G) \to H (n) = (a \in A ⟼ n (Y))$
57	55 56	sylan	$⊢ (((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land \forall z \in A m (z) = b) \land n \in G) \to H (n) = (a \in A ⟼ n (Y))$
58	57	eqeq2d	$⊢ (((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land \forall z \in A m (z) = b) \land n \in G) \to (m = H (n) \leftrightarrow m = (a \in A ⟼ n (Y)))$
59	58	rexbidva	$⊢ ((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land \forall z \in A m (z) = b) \to (\exists n \in G m = H (n) \leftrightarrow \exists n \in G m = (a \in A ⟼ n (Y)))$
60	54 59	mpbird	$⊢ ((((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \land \forall z \in A m (z) = b) \to \exists n \in G m = H (n)$
61	60	ex	$⊢ (((A \in V \land Y \in A) \land m : A ⟶ B) \land b \in B) \to (\forall z \in A m (z) = b \to \exists n \in G m = H (n))$
62	61	rexlimdva	$⊢ ((A \in V \land Y \in A) \land m : A ⟶ B) \to (\exists b \in B \forall z \in A m (z) = b \to \exists n \in G m = H (n))$
63	62	expimpd	$⊢ (A \in V \land Y \in A) \to ((m : A ⟶ B \land \exists b \in B \forall z \in A m (z) = b) \to \exists n \in G m = H (n))$
64	13 63	syl5bi	$⊢ (A \in V \land Y \in A) \to (m \in F \to \exists n \in G m = H (n))$
65	64	ralrimiv	$⊢ (A \in V \land Y \in A) \to \forall m \in F \exists n \in G m = H (n)$
66		dffo3	$⊢ H : G \underset{onto}{⟶} F \leftrightarrow (H : G ⟶ F \land \forall m \in F \exists n \in G m = H (n))$
67	4 65 66	sylanbrc	$⊢ (A \in V \land Y \in A) \to H : G \underset{onto}{⟶} F$

Metamath Proof Explorer

Theorem cfsetsnfsetfo

Proof