1arymaptfo

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

		Ref	Expression
	Hypothesis	1arymaptfv.h	No typesetting found for \|- H = ( h e. ( 1 -aryF X ) \|-> ( x e. X \|-> ( h ` { <. 0 , x >. } ) ) ) with typecode \|-
	Assertion	1arymaptfo	Could not format assertion : No typesetting found for \|- ( X e. V -> H : ( 1 -aryF X ) -onto-> ( X ^m X ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		1arymaptfv.h	Could not format H = ( h e. ( 1 -aryF X ) \|-> ( x e. X \|-> ( h ` { <. 0 , x >. } ) ) ) : No typesetting found for \|- H = ( h e. ( 1 -aryF X ) \|-> ( x e. X \|-> ( h ` { <. 0 , x >. } ) ) ) with typecode \|-
2	1	1arymaptf	Could not format ( X e. V -> H : ( 1 -aryF X ) --> ( X ^m X ) ) : No typesetting found for \|- ( X e. V -> H : ( 1 -aryF X ) --> ( X ^m X ) ) with typecode \|-
3		elmapi	$⊢ f \in (X^{X}) \to f : X ⟶ X$
4		eqid	$⊢ (a \in (X^{\{0\}}) ⟼ f (a (0))) = (a \in (X^{\{0\}}) ⟼ f (a (0)))$
5	4	1arympt1	Could not format ( ( X e. V /\ f : X --> X ) -> ( a e. ( X ^m { 0 } ) \|-> ( f ` ( a ` 0 ) ) ) e. ( 1 -aryF X ) ) : No typesetting found for \|- ( ( X e. V /\ f : X --> X ) -> ( a e. ( X ^m { 0 } ) \|-> ( f ` ( a ` 0 ) ) ) e. ( 1 -aryF X ) ) with typecode \|-
6	3 5	sylan2	Could not format ( ( X e. V /\ f e. ( X ^m X ) ) -> ( a e. ( X ^m { 0 } ) \|-> ( f ` ( a ` 0 ) ) ) e. ( 1 -aryF X ) ) : No typesetting found for \|- ( ( X e. V /\ f e. ( X ^m X ) ) -> ( a e. ( X ^m { 0 } ) \|-> ( f ` ( a ` 0 ) ) ) e. ( 1 -aryF X ) ) with typecode \|-
7		fveq2	$⊢ g = (a \in (X^{\{0\}}) ⟼ f (a (0))) \to H (g) = H ((a \in (X^{\{0\}}) ⟼ f (a (0))))$
8	7	eqeq2d	$⊢ g = (a \in (X^{\{0\}}) ⟼ f (a (0))) \to (f = H (g) \leftrightarrow f = H ((a \in (X^{\{0\}}) ⟼ f (a (0)))))$
9	8	adantl	$⊢ ((X \in V \land f \in (X^{X})) \land g = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \to (f = H (g) \leftrightarrow f = H ((a \in (X^{\{0\}}) ⟼ f (a (0)))))$
10	3	adantl	$⊢ (X \in V \land f \in (X^{X})) \to f : X ⟶ X$
11	10	feqmptd	$⊢ (X \in V \land f \in (X^{X})) \to f = (x \in X ⟼ f (x))$
12		simplr	$⊢ (((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \land x \in X) \to h = (a \in (X^{\{0\}}) ⟼ f (a (0)))$
13		fveq1	$⊢ a = \{⟨0, x⟩\} \to a (0) = \{⟨0, x⟩\} (0)$
14		c0ex	$⊢ 0 \in V$
15		vex	$⊢ x \in V$
16	14 15	fvsn	$⊢ \{⟨0, x⟩\} (0) = x$
17	13 16	eqtrdi	$⊢ a = \{⟨0, x⟩\} \to a (0) = x$
18	17	fveq2d	$⊢ a = \{⟨0, x⟩\} \to f (a (0)) = f (x)$
19	18	adantl	$⊢ ((((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \land x \in X) \land a = \{⟨0, x⟩\}) \to f (a (0)) = f (x)$
20	14	a1i	$⊢ (X \in V \land x \in X) \to 0 \in V$
21		simpr	$⊢ (X \in V \land x \in X) \to x \in X$
22	20 21	fsnd	$⊢ (X \in V \land x \in X) \to \{⟨0, x⟩\} : \{0\} ⟶ X$
23		snex	$⊢ \{0\} \in V$
24	23	a1i	$⊢ x \in X \to \{0\} \in V$
25		elmapg	$⊢ (X \in V \land \{0\} \in V) \to (\{⟨0, x⟩\} \in (X^{\{0\}}) \leftrightarrow \{⟨0, x⟩\} : \{0\} ⟶ X)$
26	24 25	sylan2	$⊢ (X \in V \land x \in X) \to (\{⟨0, x⟩\} \in (X^{\{0\}}) \leftrightarrow \{⟨0, x⟩\} : \{0\} ⟶ X)$
27	22 26	mpbird	$⊢ (X \in V \land x \in X) \to \{⟨0, x⟩\} \in (X^{\{0\}})$
28	27	ad4ant14	$⊢ (((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \land x \in X) \to \{⟨0, x⟩\} \in (X^{\{0\}})$
29		fvexd	$⊢ (((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \land x \in X) \to f (x) \in V$
30		nfv	$⊢ Ⅎ a (X \in V \land f \in (X^{X}))$
31		nfmpt1	$⊢ \underline{Ⅎ} a (a \in (X^{\{0\}}) ⟼ f (a (0)))$
32	31	nfeq2	$⊢ Ⅎ a h = (a \in (X^{\{0\}}) ⟼ f (a (0)))$
33	30 32	nfan	$⊢ Ⅎ a ((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0))))$
34		nfv	$⊢ Ⅎ a x \in X$
35	33 34	nfan	$⊢ Ⅎ a (((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \land x \in X)$
36		nfcv	$⊢ \underline{Ⅎ} a \{⟨0, x⟩\}$
37		nfcv	$⊢ \underline{Ⅎ} a f (x)$
38	12 19 28 29 35 36 37	fvmptdf	$⊢ (((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \land x \in X) \to h (\{⟨0, x⟩\}) = f (x)$
39	38	mpteq2dva	$⊢ ((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \to (x \in X ⟼ h (\{⟨0, x⟩\})) = (x \in X ⟼ f (x))$
40		simpl	$⊢ (X \in V \land f \in (X^{X})) \to X \in V$
41	40	mptexd	$⊢ (X \in V \land f \in (X^{X})) \to (x \in X ⟼ f (x)) \in V$
42	1 39 6 41	fvmptd2	$⊢ (X \in V \land f \in (X^{X})) \to H ((a \in (X^{\{0\}}) ⟼ f (a (0)))) = (x \in X ⟼ f (x))$
43	11 42	eqtr4d	$⊢ (X \in V \land f \in (X^{X})) \to f = H ((a \in (X^{\{0\}}) ⟼ f (a (0))))$
44	6 9 43	rspcedvd	Could not format ( ( X e. V /\ f e. ( X ^m X ) ) -> E. g e. ( 1 -aryF X ) f = ( H ` g ) ) : No typesetting found for \|- ( ( X e. V /\ f e. ( X ^m X ) ) -> E. g e. ( 1 -aryF X ) f = ( H ` g ) ) with typecode \|-
45	44	ralrimiva	Could not format ( X e. V -> A. f e. ( X ^m X ) E. g e. ( 1 -aryF X ) f = ( H ` g ) ) : No typesetting found for \|- ( X e. V -> A. f e. ( X ^m X ) E. g e. ( 1 -aryF X ) f = ( H ` g ) ) with typecode \|-
46		dffo3	Could not format ( H : ( 1 -aryF X ) -onto-> ( X ^m X ) <-> ( H : ( 1 -aryF X ) --> ( X ^m X ) /\ A. f e. ( X ^m X ) E. g e. ( 1 -aryF X ) f = ( H ` g ) ) ) : No typesetting found for \|- ( H : ( 1 -aryF X ) -onto-> ( X ^m X ) <-> ( H : ( 1 -aryF X ) --> ( X ^m X ) /\ A. f e. ( X ^m X ) E. g e. ( 1 -aryF X ) f = ( H ` g ) ) ) with typecode \|-
47	2 45 46	sylanbrc	Could not format ( X e. V -> H : ( 1 -aryF X ) -onto-> ( X ^m X ) ) : No typesetting found for \|- ( X e. V -> H : ( 1 -aryF X ) -onto-> ( X ^m X ) ) with typecode \|-

Metamath Proof Explorer

Theorem 1arymaptfo

Proof