Metamath Proof Explorer


Theorem 1aryfvalel

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

Ref Expression
Assertion 1aryfvalel Could not format assertion : No typesetting found for |- ( X e. V -> ( F e. ( 1 -aryF X ) <-> F : ( X ^m { 0 } ) --> X ) ) with typecode |-

Proof

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