Metamath Proof Explorer

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 
|- H = ( h e. ( 1 -aryF X ) |-> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) )
Assertion 1arymaptf1 
|- ( X e. V -> H : ( 1 -aryF X ) -1-1-> ( X ^m X ) )

Proof

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