Metamath Proof Explorer


Theorem 1aryenef

Description: The set of unary (endo)functions and the set of endofunctions are equinumerous. (Contributed by AV, 19-May-2024)

Ref Expression
Assertion 1aryenef
|- ( 1 -aryF X ) ~~ ( X ^m X )

Proof

Step Hyp Ref Expression
1 ovex
 |-  ( 1 -aryF X ) e. _V
2 1 mptex
 |-  ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) e. _V
3 2 a1i
 |-  ( X e. _V -> ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) e. _V )
4 eqid
 |-  ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) = ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) )
5 4 1arymaptf1o
 |-  ( X e. _V -> ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) )
6 f1oeq1
 |-  ( h = ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) -> ( h : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) <-> ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) ) )
7 3 5 6 spcedv
 |-  ( X e. _V -> E. h h : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) )
8 bren
 |-  ( ( 1 -aryF X ) ~~ ( X ^m X ) <-> E. h h : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) )
9 7 8 sylibr
 |-  ( X e. _V -> ( 1 -aryF X ) ~~ ( X ^m X ) )
10 0ex
 |-  (/) e. _V
11 10 enref
 |-  (/) ~~ (/)
12 11 a1i
 |-  ( -. X e. _V -> (/) ~~ (/) )
13 df-naryf
 |-  -aryF = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) )
14 13 reldmmpo
 |-  Rel dom -aryF
15 14 ovprc2
 |-  ( -. X e. _V -> ( 1 -aryF X ) = (/) )
16 reldmmap
 |-  Rel dom ^m
17 16 ovprc1
 |-  ( -. X e. _V -> ( X ^m X ) = (/) )
18 12 15 17 3brtr4d
 |-  ( -. X e. _V -> ( 1 -aryF X ) ~~ ( X ^m X ) )
19 9 18 pm2.61i
 |-  ( 1 -aryF X ) ~~ ( X ^m X )