Metamath Proof Explorer


Theorem naryfvalel

Description: An n-ary (endo)function on a set X . (Contributed by AV, 14-May-2024)

Ref Expression
Hypothesis naryfval.i I = 0 ..^ N
Assertion naryfvalel Could not format assertion : No typesetting found for |- ( ( N e. NN0 /\ X e. V ) -> ( F e. ( N -aryF X ) <-> F : ( X ^m I ) --> X ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 naryfval.i I = 0 ..^ N
2 1 naryfval Could not format ( N e. NN0 -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) : No typesetting found for |- ( N e. NN0 -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) with typecode |-
3 2 eleq2d Could not format ( N e. NN0 -> ( F e. ( N -aryF X ) <-> F e. ( X ^m ( X ^m I ) ) ) ) : No typesetting found for |- ( N e. NN0 -> ( F e. ( N -aryF X ) <-> F e. ( X ^m ( X ^m I ) ) ) ) with typecode |-
4 ovex X I V
5 elmapg X V X I V F X X I F : X I X
6 4 5 mpan2 X V F X X I F : X I X
7 3 6 sylan9bb Could not format ( ( N e. NN0 /\ X e. V ) -> ( F e. ( N -aryF X ) <-> F : ( X ^m I ) --> X ) ) : No typesetting found for |- ( ( N e. NN0 /\ X e. V ) -> ( F e. ( N -aryF X ) <-> F : ( X ^m I ) --> X ) ) with typecode |-