1arymaptf1

Description: The mapping of unary (endo)functions is a one-to-one function into the set of endofunctions. (Contributed by AV, 19-May-2024)

		Ref	Expression
	Hypothesis	1arymaptfv.h	$⊢ H = (h \in (1 -aryF X) ⟼ (x \in X ⟼ h (\{⟨0, x⟩\})))$
	Assertion	1arymaptf1	$⊢ X \in V \to H : 1 -aryF X \underset{1-1}{⟶} X^{X}$

Proof

Step	Hyp	Ref	Expression
1		1arymaptfv.h	$⊢ H = (h \in (1 -aryF X) ⟼ (x \in X ⟼ h (\{⟨0, x⟩\})))$
2	1	1arymaptf	$⊢ X \in V \to H : 1 -aryF X ⟶ X^{X}$
3	1	1arymaptfv	$⊢ f \in (1 -aryF X) \to H (f) = (x \in X ⟼ f (\{⟨0, x⟩\}))$
4	3	ad2antrl	$⊢ (X \in V \land (f \in (1 -aryF X) \land g \in (1 -aryF X))) \to H (f) = (x \in X ⟼ f (\{⟨0, x⟩\}))$
5	1	1arymaptfv	$⊢ g \in (1 -aryF X) \to H (g) = (x \in X ⟼ g (\{⟨0, x⟩\}))$
6	5	ad2antll	$⊢ (X \in V \land (f \in (1 -aryF X) \land g \in (1 -aryF X))) \to H (g) = (x \in X ⟼ g (\{⟨0, x⟩\}))$
7	4 6	eqeq12d	$⊢ (X \in V \land (f \in (1 -aryF X) \land g \in (1 -aryF X))) \to (H (f) = H (g) \leftrightarrow (x \in X ⟼ f (\{⟨0, x⟩\})) = (x \in X ⟼ g (\{⟨0, x⟩\})))$
8		fvex	$⊢ f (\{⟨0, x⟩\}) \in V$
9	8	rgenw	$⊢ \forall x \in X f (\{⟨0, x⟩\}) \in V$
10		mpteqb	$⊢ \forall x \in X f (\{⟨0, x⟩\}) \in V \to ((x \in X ⟼ f (\{⟨0, x⟩\})) = (x \in X ⟼ g (\{⟨0, x⟩\})) \leftrightarrow \forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\}))$
11	9 10	mp1i	$⊢ (X \in V \land (f \in (1 -aryF X) \land g \in (1 -aryF X))) \to ((x \in X ⟼ f (\{⟨0, x⟩\})) = (x \in X ⟼ g (\{⟨0, x⟩\})) \leftrightarrow \forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\}))$
12		1aryfvalel	$⊢ X \in V \to (f \in (1 -aryF X) \leftrightarrow f : X^{\{0\}} ⟶ X)$
13		1aryfvalel	$⊢ X \in V \to (g \in (1 -aryF X) \leftrightarrow g : X^{\{0\}} ⟶ X)$
14	12 13	anbi12d	$⊢ X \in V \to ((f \in (1 -aryF X) \land g \in (1 -aryF X)) \leftrightarrow (f : X^{\{0\}} ⟶ X \land g : X^{\{0\}} ⟶ X))$
15		ffn	$⊢ f : X^{\{0\}} ⟶ X \to f Fn (X^{\{0\}})$
16	15	adantr	$⊢ (f : X^{\{0\}} ⟶ X \land g : X^{\{0\}} ⟶ X) \to f Fn (X^{\{0\}})$
17	16	3ad2ant2	$⊢ (X \in V \land (f : X^{\{0\}} ⟶ X \land g : X^{\{0\}} ⟶ X) \land \forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\})) \to f Fn (X^{\{0\}})$
18		ffn	$⊢ g : X^{\{0\}} ⟶ X \to g Fn (X^{\{0\}})$
19	18	adantl	$⊢ (f : X^{\{0\}} ⟶ X \land g : X^{\{0\}} ⟶ X) \to g Fn (X^{\{0\}})$
20	19	3ad2ant2	$⊢ (X \in V \land (f : X^{\{0\}} ⟶ X \land g : X^{\{0\}} ⟶ X) \land \forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\})) \to g Fn (X^{\{0\}})$
21		elmapi	$⊢ y \in (X^{\{0\}}) \to y : \{0\} ⟶ X$
22		c0ex	$⊢ 0 \in V$
23	22	fsn2	$⊢ y : \{0\} ⟶ X \leftrightarrow (y (0) \in X \land y = \{⟨0, y (0)⟩\})$
24	21 23	sylib	$⊢ y \in (X^{\{0\}}) \to (y (0) \in X \land y = \{⟨0, y (0)⟩\})$
25		opeq2	$⊢ x = y (0) \to ⟨0, x⟩ = ⟨0, y (0)⟩$
26	25	sneqd	$⊢ x = y (0) \to \{⟨0, x⟩\} = \{⟨0, y (0)⟩\}$
27	26	fveq2d	$⊢ x = y (0) \to f (\{⟨0, x⟩\}) = f (\{⟨0, y (0)⟩\})$
28	26	fveq2d	$⊢ x = y (0) \to g (\{⟨0, x⟩\}) = g (\{⟨0, y (0)⟩\})$
29	27 28	eqeq12d	$⊢ x = y (0) \to (f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\}) \leftrightarrow f (\{⟨0, y (0)⟩\}) = g (\{⟨0, y (0)⟩\}))$
30	29	rspccv	$⊢ \forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\}) \to (y (0) \in X \to f (\{⟨0, y (0)⟩\}) = g (\{⟨0, y (0)⟩\}))$
31	30	3ad2ant3	$⊢ (X \in V \land (f : X^{\{0\}} ⟶ X \land g : X^{\{0\}} ⟶ X) \land \forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\})) \to (y (0) \in X \to f (\{⟨0, y (0)⟩\}) = g (\{⟨0, y (0)⟩\}))$
32	31	com12	$⊢ y (0) \in X \to ((X \in V \land (f : X^{\{0\}} ⟶ X \land g : X^{\{0\}} ⟶ X) \land \forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\})) \to f (\{⟨0, y (0)⟩\}) = g (\{⟨0, y (0)⟩\}))$
33	32	adantr	$⊢ (y (0) \in X \land y = \{⟨0, y (0)⟩\}) \to ((X \in V \land (f : X^{\{0\}} ⟶ X \land g : X^{\{0\}} ⟶ X) \land \forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\})) \to f (\{⟨0, y (0)⟩\}) = g (\{⟨0, y (0)⟩\}))$
34		fveq2	$⊢ y = \{⟨0, y (0)⟩\} \to f (y) = f (\{⟨0, y (0)⟩\})$
35		fveq2	$⊢ y = \{⟨0, y (0)⟩\} \to g (y) = g (\{⟨0, y (0)⟩\})$
36	34 35	eqeq12d	$⊢ y = \{⟨0, y (0)⟩\} \to (f (y) = g (y) \leftrightarrow f (\{⟨0, y (0)⟩\}) = g (\{⟨0, y (0)⟩\}))$
37	36	adantl	$⊢ (y (0) \in X \land y = \{⟨0, y (0)⟩\}) \to (f (y) = g (y) \leftrightarrow f (\{⟨0, y (0)⟩\}) = g (\{⟨0, y (0)⟩\}))$
38	33 37	sylibrd	$⊢ (y (0) \in X \land y = \{⟨0, y (0)⟩\}) \to ((X \in V \land (f : X^{\{0\}} ⟶ X \land g : X^{\{0\}} ⟶ X) \land \forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\})) \to f (y) = g (y))$
39	24 38	syl	$⊢ y \in (X^{\{0\}}) \to ((X \in V \land (f : X^{\{0\}} ⟶ X \land g : X^{\{0\}} ⟶ X) \land \forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\})) \to f (y) = g (y))$
40	39	impcom	$⊢ ((X \in V \land (f : X^{\{0\}} ⟶ X \land g : X^{\{0\}} ⟶ X) \land \forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\})) \land y \in (X^{\{0\}})) \to f (y) = g (y)$
41	17 20 40	eqfnfvd	$⊢ (X \in V \land (f : X^{\{0\}} ⟶ X \land g : X^{\{0\}} ⟶ X) \land \forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\})) \to f = g$
42	41	3exp	$⊢ X \in V \to ((f : X^{\{0\}} ⟶ X \land g : X^{\{0\}} ⟶ X) \to (\forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\}) \to f = g))$
43	14 42	sylbid	$⊢ X \in V \to ((f \in (1 -aryF X) \land g \in (1 -aryF X)) \to (\forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\}) \to f = g))$
44	43	imp	$⊢ (X \in V \land (f \in (1 -aryF X) \land g \in (1 -aryF X))) \to (\forall x \in X f (\{⟨0, x⟩\}) = g (\{⟨0, x⟩\}) \to f = g)$
45	11 44	sylbid	$⊢ (X \in V \land (f \in (1 -aryF X) \land g \in (1 -aryF X))) \to ((x \in X ⟼ f (\{⟨0, x⟩\})) = (x \in X ⟼ g (\{⟨0, x⟩\})) \to f = g)$
46	7 45	sylbid	$⊢ (X \in V \land (f \in (1 -aryF X) \land g \in (1 -aryF X))) \to (H (f) = H (g) \to f = g)$
47	46	ralrimivva	$⊢ X \in V \to \forall f \in (1 -aryF X) \forall g \in (1 -aryF X) (H (f) = H (g) \to f = g)$
48		dff13	$⊢ H : 1 -aryF X \underset{1-1}{⟶} X^{X} \leftrightarrow (H : 1 -aryF X ⟶ X^{X} \land \forall f \in (1 -aryF X) \forall g \in (1 -aryF X) (H (f) = H (g) \to f = g))$
49	2 47 48	sylanbrc	$⊢ X \in V \to H : 1 -aryF X \underset{1-1}{⟶} X^{X}$

Metamath Proof Explorer

Theorem 1arymaptf1

Proof