Theorem 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	No typesetting found for |- H = ( h e. ( 1 -aryF X ) |-> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) ) with typecode |-
Assertion	1arymaptf1	Could not format assertion : No typesetting found for |- ( X e. V -> H : ( 1 -aryF X ) -1-1-> ( 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	1	1arymaptfv	Could not format ( f e. ( 1 -aryF X ) -> ( H ` f ) = ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) : No typesetting found for |- ( f e. ( 1 -aryF X ) -> ( H ` f ) = ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) with typecode |-
4	3	ad2antrl	Could not format ( ( X e. V /\ ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) ) -> ( H ` f ) = ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) ) -> ( H ` f ) = ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) with typecode |-
5	1	1arymaptfv	Could not format ( g e. ( 1 -aryF X ) -> ( H ` g ) = ( x e. X |-> ( g ` { <. 0 , x >. } ) ) ) : No typesetting found for |- ( g e. ( 1 -aryF X ) -> ( H ` g ) = ( x e. X |-> ( g ` { <. 0 , x >. } ) ) ) with typecode |-
6	5	ad2antll	Could not format ( ( X e. V /\ ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) ) -> ( H ` g ) = ( x e. X |-> ( g ` { <. 0 , x >. } ) ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) ) -> ( H ` g ) = ( x e. X |-> ( g ` { <. 0 , x >. } ) ) ) with typecode |-
7	4 6	eqeq12d	Could not format ( ( X e. V /\ ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) ) -> ( ( H ` f ) = ( H ` g ) <-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) = ( x e. X |-> ( g ` { <. 0 , x >. } ) ) ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) ) -> ( ( H ` f ) = ( H ` g ) <-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) = ( x e. X |-> ( g ` { <. 0 , x >. } ) ) ) ) with typecode |-
8		fvex	$$⊢f\left(\left\{⟨0,x⟩\right\}\right)\in \mathrm{V}$$
9	8	rgenw	$$⊢\forall x\in Xf\left(\left\{⟨0,x⟩\right\}\right)\in \mathrm{V}$$
10		mpteqb	$$⊢\forall x\in Xf\left(\left\{⟨0,x⟩\right\}\right)\in \mathrm{V}\to \left(\left(x\in X⟼f\left(\left\{⟨0,x⟩\right\}\right)\right)=\left(x\in X⟼g\left(\left\{⟨0,x⟩\right\}\right)\right)\leftrightarrow \forall x\in Xf\left(\left\{⟨0,x⟩\right\}\right)=g\left(\left\{⟨0,x⟩\right\}\right)\right)$$
11	9 10	mp1i	Could not format ( ( X e. V /\ ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) ) -> ( ( x e. X |-> ( f ` { <. 0 , x >. } ) ) = ( x e. X |-> ( g ` { <. 0 , x >. } ) ) <-> A. x e. X ( f ` { <. 0 , x >. } ) = ( g ` { <. 0 , x >. } ) ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) ) -> ( ( x e. X |-> ( f ` { <. 0 , x >. } ) ) = ( x e. X |-> ( g ` { <. 0 , x >. } ) ) <-> A. x e. X ( f ` { <. 0 , x >. } ) = ( g ` { <. 0 , x >. } ) ) ) with typecode |-
12		1aryfvalel	Could not format ( X e. V -> ( f e. ( 1 -aryF X ) <-> f : ( X ^m { 0 } ) --> X ) ) : No typesetting found for |- ( X e. V -> ( f e. ( 1 -aryF X ) <-> f : ( X ^m { 0 } ) --> X ) ) with typecode |-
13		1aryfvalel	Could not format ( X e. V -> ( g e. ( 1 -aryF X ) <-> g : ( X ^m { 0 } ) --> X ) ) : No typesetting found for |- ( X e. V -> ( g e. ( 1 -aryF X ) <-> g : ( X ^m { 0 } ) --> X ) ) with typecode |-
14	12 13	anbi12d	Could not format ( X e. V -> ( ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) <-> ( f : ( X ^m { 0 } ) --> X /\ g : ( X ^m { 0 } ) --> X ) ) ) : No typesetting found for |- ( X e. V -> ( ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) <-> ( f : ( X ^m { 0 } ) --> X /\ g : ( X ^m { 0 } ) --> X ) ) ) with typecode |-
15		ffn	$$⊢f:X^{\left\{0\right\}}⟶X\to fFn\left(X^{\left\{0\right\}}\right)$$
16	15	adantr	$$⊢\left(f:X^{\left\{0\right\}}⟶X\wedge g:X^{\left\{0\right\}}⟶X\right)\to fFn\left(X^{\left\{0\right\}}\right)$$
17	16	3ad2ant2	$$⊢\left(X\in V\wedge \left(f:X^{\left\{0\right\}}⟶X\wedge g:X^{\left\{0\right\}}⟶X\right)\wedge \forall x\in Xf\left(\left\{⟨0,x⟩\right\}\right)=g\left(\left\{⟨0,x⟩\right\}\right)\right)\to fFn\left(X^{\left\{0\right\}}\right)$$
18		ffn	$$⊢g:X^{\left\{0\right\}}⟶X\to gFn\left(X^{\left\{0\right\}}\right)$$
19	18	adantl	$$⊢\left(f:X^{\left\{0\right\}}⟶X\wedge g:X^{\left\{0\right\}}⟶X\right)\to gFn\left(X^{\left\{0\right\}}\right)$$
20	19	3ad2ant2	$$⊢\left(X\in V\wedge \left(f:X^{\left\{0\right\}}⟶X\wedge g:X^{\left\{0\right\}}⟶X\right)\wedge \forall x\in Xf\left(\left\{⟨0,x⟩\right\}\right)=g\left(\left\{⟨0,x⟩\right\}\right)\right)\to gFn\left(X^{\left\{0\right\}}\right)$$
21		elmapi	$$⊢y\in \left(X^{\left\{0\right\}}\right)\to y:\left\{0\right\}⟶X$$
22		c0ex	$$⊢0\in \mathrm{V}$$
23	22	fsn2	$$⊢y:\left\{0\right\}⟶X\leftrightarrow \left(y\left(0\right)\in X\wedge y=\left\{⟨0,y\left(0\right)⟩\right\}\right)$$
24	21 23	sylib	$$⊢y\in \left(X^{\left\{0\right\}}\right)\to \left(y\left(0\right)\in X\wedge y=\left\{⟨0,y\left(0\right)⟩\right\}\right)$$
25		opeq2	$$⊢x=y\left(0\right)\to ⟨0,x⟩=⟨0,y\left(0\right)⟩$$
26	25	sneqd	$$⊢x=y\left(0\right)\to \left\{⟨0,x⟩\right\}=\left\{⟨0,y\left(0\right)⟩\right\}$$
27	26	fveq2d	$$⊢x=y\left(0\right)\to f\left(\left\{⟨0,x⟩\right\}\right)=f\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)$$
28	26	fveq2d	$$⊢x=y\left(0\right)\to g\left(\left\{⟨0,x⟩\right\}\right)=g\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)$$
29	27 28	eqeq12d	$$⊢x=y\left(0\right)\to \left(f\left(\left\{⟨0,x⟩\right\}\right)=g\left(\left\{⟨0,x⟩\right\}\right)\leftrightarrow f\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)=g\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)\right)$$
30	29	rspccv	$$⊢\forall x\in Xf\left(\left\{⟨0,x⟩\right\}\right)=g\left(\left\{⟨0,x⟩\right\}\right)\to \left(y\left(0\right)\in X\to f\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)=g\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)\right)$$
31	30	3ad2ant3	$$⊢\left(X\in V\wedge \left(f:X^{\left\{0\right\}}⟶X\wedge g:X^{\left\{0\right\}}⟶X\right)\wedge \forall x\in Xf\left(\left\{⟨0,x⟩\right\}\right)=g\left(\left\{⟨0,x⟩\right\}\right)\right)\to \left(y\left(0\right)\in X\to f\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)=g\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)\right)$$
32	31	com12	$$⊢y\left(0\right)\in X\to \left(\left(X\in V\wedge \left(f:X^{\left\{0\right\}}⟶X\wedge g:X^{\left\{0\right\}}⟶X\right)\wedge \forall x\in Xf\left(\left\{⟨0,x⟩\right\}\right)=g\left(\left\{⟨0,x⟩\right\}\right)\right)\to f\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)=g\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)\right)$$
33	32	adantr	$$⊢\left(y\left(0\right)\in X\wedge y=\left\{⟨0,y\left(0\right)⟩\right\}\right)\to \left(\left(X\in V\wedge \left(f:X^{\left\{0\right\}}⟶X\wedge g:X^{\left\{0\right\}}⟶X\right)\wedge \forall x\in Xf\left(\left\{⟨0,x⟩\right\}\right)=g\left(\left\{⟨0,x⟩\right\}\right)\right)\to f\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)=g\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)\right)$$
34		fveq2	$$⊢y=\left\{⟨0,y\left(0\right)⟩\right\}\to f\left(y\right)=f\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)$$
35		fveq2	$$⊢y=\left\{⟨0,y\left(0\right)⟩\right\}\to g\left(y\right)=g\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)$$
36	34 35	eqeq12d	$$⊢y=\left\{⟨0,y\left(0\right)⟩\right\}\to \left(f\left(y\right)=g\left(y\right)\leftrightarrow f\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)=g\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)\right)$$
37	36	adantl	$$⊢\left(y\left(0\right)\in X\wedge y=\left\{⟨0,y\left(0\right)⟩\right\}\right)\to \left(f\left(y\right)=g\left(y\right)\leftrightarrow f\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)=g\left(\left\{⟨0,y\left(0\right)⟩\right\}\right)\right)$$
38	33 37	sylibrd	$$⊢\left(y\left(0\right)\in X\wedge y=\left\{⟨0,y\left(0\right)⟩\right\}\right)\to \left(\left(X\in V\wedge \left(f:X^{\left\{0\right\}}⟶X\wedge g:X^{\left\{0\right\}}⟶X\right)\wedge \forall x\in Xf\left(\left\{⟨0,x⟩\right\}\right)=g\left(\left\{⟨0,x⟩\right\}\right)\right)\to f\left(y\right)=g\left(y\right)\right)$$
39	24 38	syl	$$⊢y\in \left(X^{\left\{0\right\}}\right)\to \left(\left(X\in V\wedge \left(f:X^{\left\{0\right\}}⟶X\wedge g:X^{\left\{0\right\}}⟶X\right)\wedge \forall x\in Xf\left(\left\{⟨0,x⟩\right\}\right)=g\left(\left\{⟨0,x⟩\right\}\right)\right)\to f\left(y\right)=g\left(y\right)\right)$$
40	39	impcom	$$⊢\left(\left(X\in V\wedge \left(f:X^{\left\{0\right\}}⟶X\wedge g:X^{\left\{0\right\}}⟶X\right)\wedge \forall x\in Xf\left(\left\{⟨0,x⟩\right\}\right)=g\left(\left\{⟨0,x⟩\right\}\right)\right)\wedge y\in \left(X^{\left\{0\right\}}\right)\right)\to f\left(y\right)=g\left(y\right)$$
41	17 20 40	eqfnfvd	$$⊢\left(X\in V\wedge \left(f:X^{\left\{0\right\}}⟶X\wedge g:X^{\left\{0\right\}}⟶X\right)\wedge \forall x\in Xf\left(\left\{⟨0,x⟩\right\}\right)=g\left(\left\{⟨0,x⟩\right\}\right)\right)\to f=g$$
42	41	3exp	$$⊢X\in V\to \left(\left(f:X^{\left\{0\right\}}⟶X\wedge g:X^{\left\{0\right\}}⟶X\right)\to \left(\forall x\in Xf\left(\left\{⟨0,x⟩\right\}\right)=g\left(\left\{⟨0,x⟩\right\}\right)\to f=g\right)\right)$$
43	14 42	sylbid	Could not format ( X e. V -> ( ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) -> ( A. x e. X ( f ` { <. 0 , x >. } ) = ( g ` { <. 0 , x >. } ) -> f = g ) ) ) : No typesetting found for |- ( X e. V -> ( ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) -> ( A. x e. X ( f ` { <. 0 , x >. } ) = ( g ` { <. 0 , x >. } ) -> f = g ) ) ) with typecode |-
44	43	imp	Could not format ( ( X e. V /\ ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) ) -> ( A. x e. X ( f ` { <. 0 , x >. } ) = ( g ` { <. 0 , x >. } ) -> f = g ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) ) -> ( A. x e. X ( f ` { <. 0 , x >. } ) = ( g ` { <. 0 , x >. } ) -> f = g ) ) with typecode |-
45	11 44	sylbid	Could not format ( ( X e. V /\ ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) ) -> ( ( x e. X |-> ( f ` { <. 0 , x >. } ) ) = ( x e. X |-> ( g ` { <. 0 , x >. } ) ) -> f = g ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) ) -> ( ( x e. X |-> ( f ` { <. 0 , x >. } ) ) = ( x e. X |-> ( g ` { <. 0 , x >. } ) ) -> f = g ) ) with typecode |-
46	7 45	sylbid	Could not format ( ( X e. V /\ ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) ) -> ( ( H ` f ) = ( H ` g ) -> f = g ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 1 -aryF X ) /\ g e. ( 1 -aryF X ) ) ) -> ( ( H ` f ) = ( H ` g ) -> f = g ) ) with typecode |-
47	46	ralrimivva	Could not format ( X e. V -> A. f e. ( 1 -aryF X ) A. g e. ( 1 -aryF X ) ( ( H ` f ) = ( H ` g ) -> f = g ) ) : No typesetting found for |- ( X e. V -> A. f e. ( 1 -aryF X ) A. g e. ( 1 -aryF X ) ( ( H ` f ) = ( H ` g ) -> f = g ) ) with typecode |-
48		dff13	Could not format ( H : ( 1 -aryF X ) -1-1-> ( X ^m X ) <-> ( H : ( 1 -aryF X ) --> ( X ^m X ) /\ A. f e. ( 1 -aryF X ) A. g e. ( 1 -aryF X ) ( ( H ` f ) = ( H ` g ) -> f = g ) ) ) : No typesetting found for |- ( H : ( 1 -aryF X ) -1-1-> ( X ^m X ) <-> ( H : ( 1 -aryF X ) --> ( X ^m X ) /\ A. f e. ( 1 -aryF X ) A. g e. ( 1 -aryF X ) ( ( H ` f ) = ( H ` g ) -> f = g ) ) ) with typecode |-
49	2 47 48	sylanbrc	Could not format ( X e. V -> H : ( 1 -aryF X ) -1-1-> ( X ^m X ) ) : No typesetting found for |- ( X e. V -> H : ( 1 -aryF X ) -1-1-> ( X ^m X ) ) with typecode |-