Metamath Proof Explorer


Theorem 2aryfvalel

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

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

Proof

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