Metamath Proof Explorer

Theorem 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 
|- H = ( h e. ( 1 -aryF X ) |-> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) )
Assertion 1arymaptfo 
|- ( X e. V -> H : ( 1 -aryF X ) -onto-> ( 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 elmapi 
 |-  ( f e. ( X ^m X ) -> f : X --> X )
4 eqid 
 |-  ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) = ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) )
5 4 1arympt1 
 |-  ( ( X e. V /\ f : X --> X ) -> ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) e. ( 1 -aryF X ) )
6 3 5 sylan2 
 |-  ( ( X e. V /\ f e. ( X ^m X ) ) -> ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) e. ( 1 -aryF X ) )
7 fveq2 
 |-  ( g = ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) -> ( H ` g ) = ( H ` ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) ) )
8 7 eqeq2d 
 |-  ( g = ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) -> ( f = ( H ` g ) <-> f = ( H ` ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) ) ) )
9 8 adantl 
 |-  ( ( ( X e. V /\ f e. ( X ^m X ) ) /\ g = ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) ) -> ( f = ( H ` g ) <-> f = ( H ` ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) ) ) )
10 3 adantl 
 |-  ( ( X e. V /\ f e. ( X ^m X ) ) -> f : X --> X )
11 10 feqmptd 
 |-  ( ( X e. V /\ f e. ( X ^m X ) ) -> f = ( x e. X |-> ( f ` x ) ) )
12 simplr 
 |-  ( ( ( ( X e. V /\ f e. ( X ^m X ) ) /\ h = ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) ) /\ x e. X ) -> h = ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) )
13 fveq1 
 |-  ( a = { <. 0 , x >. } -> ( a ` 0 ) = ( { <. 0 , x >. } ` 0 ) )
14 c0ex 
 |-  0 e. _V
15 vex 
 |-  x e. _V
16 14 15 fvsn 
 |-  ( { <. 0 , x >. } ` 0 ) = x
17 13 16 eqtrdi 
 |-  ( a = { <. 0 , x >. } -> ( a ` 0 ) = x )
18 17 fveq2d 
 |-  ( a = { <. 0 , x >. } -> ( f ` ( a ` 0 ) ) = ( f ` x ) )
19 18 adantl 
 |-  ( ( ( ( ( X e. V /\ f e. ( X ^m X ) ) /\ h = ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) ) /\ x e. X ) /\ a = { <. 0 , x >. } ) -> ( f ` ( a ` 0 ) ) = ( f ` x ) )
20 14 a1i 
 |-  ( ( X e. V /\ x e. X ) -> 0 e. _V )
21 simpr 
 |-  ( ( X e. V /\ x e. X ) -> x e. X )
22 20 21 fsnd 
 |-  ( ( X e. V /\ x e. X ) -> { <. 0 , x >. } : { 0 } --> X )
23 snex 
 |-  { 0 } e. _V
24 23 a1i 
 |-  ( x e. X -> { 0 } e. _V )
25 elmapg 
 |-  ( ( X e. V /\ { 0 } e. _V ) -> ( { <. 0 , x >. } e. ( X ^m { 0 } ) <-> { <. 0 , x >. } : { 0 } --> X ) )
26 24 25 sylan2 
 |-  ( ( X e. V /\ x e. X ) -> ( { <. 0 , x >. } e. ( X ^m { 0 } ) <-> { <. 0 , x >. } : { 0 } --> X ) )
27 22 26 mpbird 
 |-  ( ( X e. V /\ x e. X ) -> { <. 0 , x >. } e. ( X ^m { 0 } ) )
28 27 ad4ant14 
 |-  ( ( ( ( X e. V /\ f e. ( X ^m X ) ) /\ h = ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) ) /\ x e. X ) -> { <. 0 , x >. } e. ( X ^m { 0 } ) )
29 fvexd 
 |-  ( ( ( ( X e. V /\ f e. ( X ^m X ) ) /\ h = ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) ) /\ x e. X ) -> ( f ` x ) e. _V )
30 nfv 
 |-  F/ a ( X e. V /\ f e. ( X ^m X ) )
31 nfmpt1 
 |-  F/_ a ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) )
32 31 nfeq2 
 |-  F/ a h = ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) )
33 30 32 nfan 
 |-  F/ a ( ( X e. V /\ f e. ( X ^m X ) ) /\ h = ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) )
34 nfv 
 |-  F/ a x e. X
35 33 34 nfan 
 |-  F/ a ( ( ( X e. V /\ f e. ( X ^m X ) ) /\ h = ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) ) /\ x e. X )
36 nfcv 
 |-  F/_ a { <. 0 , x >. }
37 nfcv 
 |-  F/_ a ( f ` x )
38 12 19 28 29 35 36 37 fvmptdf 
 |-  ( ( ( ( X e. V /\ f e. ( X ^m X ) ) /\ h = ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) ) /\ x e. X ) -> ( h ` { <. 0 , x >. } ) = ( f ` x ) )
39 38 mpteq2dva 
 |-  ( ( ( X e. V /\ f e. ( X ^m X ) ) /\ h = ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) ) -> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) = ( x e. X |-> ( f ` x ) ) )
40 simpl 
 |-  ( ( X e. V /\ f e. ( X ^m X ) ) -> X e. V )
41 40 mptexd 
 |-  ( ( X e. V /\ f e. ( X ^m X ) ) -> ( x e. X |-> ( f ` x ) ) e. _V )
42 1 39 6 41 fvmptd2 
 |-  ( ( X e. V /\ f e. ( X ^m X ) ) -> ( H ` ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) ) = ( x e. X |-> ( f ` x ) ) )
43 11 42 eqtr4d 
 |-  ( ( X e. V /\ f e. ( X ^m X ) ) -> f = ( H ` ( a e. ( X ^m { 0 } ) |-> ( f ` ( a ` 0 ) ) ) ) )
44 6 9 43 rspcedvd 
 |-  ( ( X e. V /\ f e. ( X ^m X ) ) -> E. g e. ( 1 -aryF X ) f = ( H ` g ) )
45 44 ralrimiva 
 |-  ( X e. V -> A. f e. ( X ^m X ) E. g e. ( 1 -aryF X ) f = ( H ` g ) )
46 dffo3 
 |-  ( 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 ) ) )
47 2 45 46 sylanbrc 
 |-  ( X e. V -> H : ( 1 -aryF X ) -onto-> ( X ^m X ) )