Metamath Proof Explorer


Theorem 1aryfvalel

Description: A unary (endo)function on a set X . (Contributed by AV, 15-May-2024)

Ref Expression
Assertion 1aryfvalel
|- ( X e. V -> ( F e. ( 1 -aryF X ) <-> F : ( X ^m { 0 } ) --> X ) )

Proof

Step Hyp Ref Expression
1 1nn0
 |-  1 e. NN0
2 fzo01
 |-  ( 0 ..^ 1 ) = { 0 }
3 2 eqcomi
 |-  { 0 } = ( 0 ..^ 1 )
4 3 naryfvalel
 |-  ( ( 1 e. NN0 /\ X e. V ) -> ( F e. ( 1 -aryF X ) <-> F : ( X ^m { 0 } ) --> X ) )
5 1 4 mpan
 |-  ( X e. V -> ( F e. ( 1 -aryF X ) <-> F : ( X ^m { 0 } ) --> X ) )