cfsetsnfsetf1

Description: The mapping of the class of singleton functions into the class of constant functions is an injection. (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	cfsetsnfsetf1	$⊢ (A \in V \land Y \in A) \to H : G \underset{1-1}{⟶} 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	1 2 3	cfsetsnfsetfv	$⊢ (A \in V \land m \in G) \to H (m) = (a \in A ⟼ m (Y))$
6	5	ad2ant2r	$⊢ ((A \in V \land Y \in A) \land (m \in G \land n \in G)) \to H (m) = (a \in A ⟼ m (Y))$
7	1 2 3	cfsetsnfsetfv	$⊢ (A \in V \land n \in G) \to H (n) = (a \in A ⟼ n (Y))$
8	7	ad2ant2rl	$⊢ ((A \in V \land Y \in A) \land (m \in G \land n \in G)) \to H (n) = (a \in A ⟼ n (Y))$
9	6 8	eqeq12d	$⊢ ((A \in V \land Y \in A) \land (m \in G \land n \in G)) \to (H (m) = H (n) \leftrightarrow (a \in A ⟼ m (Y)) = (a \in A ⟼ n (Y)))$
10		fvexd	$⊢ (((A \in V \land Y \in A) \land (m \in G \land n \in G)) \land a \in A) \to m (Y) \in V$
11	10	ralrimiva	$⊢ ((A \in V \land Y \in A) \land (m \in G \land n \in G)) \to \forall a \in A m (Y) \in V$
12		mpteqb	$⊢ \forall a \in A m (Y) \in V \to ((a \in A ⟼ m (Y)) = (a \in A ⟼ n (Y)) \leftrightarrow \forall a \in A m (Y) = n (Y))$
13	11 12	syl	$⊢ ((A \in V \land Y \in A) \land (m \in G \land n \in G)) \to ((a \in A ⟼ m (Y)) = (a \in A ⟼ n (Y)) \leftrightarrow \forall a \in A m (Y) = n (Y))$
14		simplr	$⊢ ((A \in V \land Y \in A) \land (m \in G \land n \in G)) \to Y \in A$
15		idd	$⊢ (((A \in V \land Y \in A) \land (m \in G \land n \in G)) \land a = Y) \to (m (Y) = n (Y) \to m (Y) = n (Y))$
16	14 15	rspcimdv	$⊢ ((A \in V \land Y \in A) \land (m \in G \land n \in G)) \to (\forall a \in A m (Y) = n (Y) \to m (Y) = n (Y))$
17		vex	$⊢ m \in V$
18		feq1	$⊢ x = m \to (x : \{Y\} ⟶ B \leftrightarrow m : \{Y\} ⟶ B)$
19	17 18 2	elab2	$⊢ m \in G \leftrightarrow m : \{Y\} ⟶ B$
20		vex	$⊢ n \in V$
21		feq1	$⊢ x = n \to (x : \{Y\} ⟶ B \leftrightarrow n : \{Y\} ⟶ B)$
22	20 21 2	elab2	$⊢ n \in G \leftrightarrow n : \{Y\} ⟶ B$
23	19 22	anbi12i	$⊢ (m \in G \land n \in G) \leftrightarrow (m : \{Y\} ⟶ B \land n : \{Y\} ⟶ B)$
24		simp3	$⊢ ((A \in V \land Y \in A) \land (m : \{Y\} ⟶ B \land n : \{Y\} ⟶ B) \land m (Y) = n (Y)) \to m (Y) = n (Y)$
25		simp1r	$⊢ ((A \in V \land Y \in A) \land (m : \{Y\} ⟶ B \land n : \{Y\} ⟶ B) \land m (Y) = n (Y)) \to Y \in A$
26		fveq2	$⊢ y = Y \to m (y) = m (Y)$
27		fveq2	$⊢ y = Y \to n (y) = n (Y)$
28	26 27	eqeq12d	$⊢ y = Y \to (m (y) = n (y) \leftrightarrow m (Y) = n (Y))$
29	28	ralsng	$⊢ Y \in A \to (\forall y \in \{Y\} m (y) = n (y) \leftrightarrow m (Y) = n (Y))$
30	25 29	syl	$⊢ ((A \in V \land Y \in A) \land (m : \{Y\} ⟶ B \land n : \{Y\} ⟶ B) \land m (Y) = n (Y)) \to (\forall y \in \{Y\} m (y) = n (y) \leftrightarrow m (Y) = n (Y))$
31	24 30	mpbird	$⊢ ((A \in V \land Y \in A) \land (m : \{Y\} ⟶ B \land n : \{Y\} ⟶ B) \land m (Y) = n (Y)) \to \forall y \in \{Y\} m (y) = n (y)$
32		ffn	$⊢ m : \{Y\} ⟶ B \to m Fn \{Y\}$
33		ffn	$⊢ n : \{Y\} ⟶ B \to n Fn \{Y\}$
34	32 33	anim12i	$⊢ (m : \{Y\} ⟶ B \land n : \{Y\} ⟶ B) \to (m Fn \{Y\} \land n Fn \{Y\})$
35	34	3ad2ant2	$⊢ ((A \in V \land Y \in A) \land (m : \{Y\} ⟶ B \land n : \{Y\} ⟶ B) \land m (Y) = n (Y)) \to (m Fn \{Y\} \land n Fn \{Y\})$
36		eqfnfv	$⊢ (m Fn \{Y\} \land n Fn \{Y\}) \to (m = n \leftrightarrow \forall y \in \{Y\} m (y) = n (y))$
37	35 36	syl	$⊢ ((A \in V \land Y \in A) \land (m : \{Y\} ⟶ B \land n : \{Y\} ⟶ B) \land m (Y) = n (Y)) \to (m = n \leftrightarrow \forall y \in \{Y\} m (y) = n (y))$
38	31 37	mpbird	$⊢ ((A \in V \land Y \in A) \land (m : \{Y\} ⟶ B \land n : \{Y\} ⟶ B) \land m (Y) = n (Y)) \to m = n$
39	38	3exp	$⊢ (A \in V \land Y \in A) \to ((m : \{Y\} ⟶ B \land n : \{Y\} ⟶ B) \to (m (Y) = n (Y) \to m = n))$
40	23 39	syl5bi	$⊢ (A \in V \land Y \in A) \to ((m \in G \land n \in G) \to (m (Y) = n (Y) \to m = n))$
41	40	imp	$⊢ ((A \in V \land Y \in A) \land (m \in G \land n \in G)) \to (m (Y) = n (Y) \to m = n)$
42	16 41	syld	$⊢ ((A \in V \land Y \in A) \land (m \in G \land n \in G)) \to (\forall a \in A m (Y) = n (Y) \to m = n)$
43	13 42	sylbid	$⊢ ((A \in V \land Y \in A) \land (m \in G \land n \in G)) \to ((a \in A ⟼ m (Y)) = (a \in A ⟼ n (Y)) \to m = n)$
44	9 43	sylbid	$⊢ ((A \in V \land Y \in A) \land (m \in G \land n \in G)) \to (H (m) = H (n) \to m = n)$
45	44	ralrimivva	$⊢ (A \in V \land Y \in A) \to \forall m \in G \forall n \in G (H (m) = H (n) \to m = n)$
46		dff13	$⊢ H : G \underset{1-1}{⟶} F \leftrightarrow (H : G ⟶ F \land \forall m \in G \forall n \in G (H (m) = H (n) \to m = n))$
47	4 45 46	sylanbrc	$⊢ (A \in V \land Y \in A) \to H : G \underset{1-1}{⟶} F$

Metamath Proof Explorer

Theorem cfsetsnfsetf1

Proof