Metamath Proof Explorer

Theorem 2aryenef

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

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

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( 2 -aryF X ) e. _V
2 1 mptex 
 |-  ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) e. _V
3 2 a1i 
 |-  ( X e. _V -> ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) e. _V )
4 eqid 
 |-  ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) = ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) )
5 4 2arymaptf1o 
 |-  ( X e. _V -> ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) )
6 f1oeq1 
 |-  ( h = ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) -> ( h : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) <-> ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) ) )
7 3 5 6 spcedv 
 |-  ( X e. _V -> E. h h : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) )
8 bren 
 |-  ( ( 2 -aryF X ) ~~ ( X ^m ( X X. X ) ) <-> E. h h : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) )
9 7 8 sylibr 
 |-  ( X e. _V -> ( 2 -aryF X ) ~~ ( X ^m ( X X. 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 -> ( 2 -aryF X ) = (/) )
16 reldmmap 
 |-  Rel dom ^m
17 16 ovprc1 
 |-  ( -. X e. _V -> ( X ^m ( X X. X ) ) = (/) )
18 12 15 17 3brtr4d 
 |-  ( -. X e. _V -> ( 2 -aryF X ) ~~ ( X ^m ( X X. X ) ) )
19 9 18 pm2.61i 
 |-  ( 2 -aryF X ) ~~ ( X ^m ( X X. X ) )