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 Could not format assertion : No typesetting found for |- ( 2 -aryF X ) ~~ ( X ^m ( X X. X ) ) with typecode |-

Proof

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