Metamath Proof Explorer


Theorem naryfval

Description: The set of the n-ary (endo)functions on a class X . (Contributed by AV, 13-May-2024)

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

Proof

Step Hyp Ref Expression
1 naryfval.i I = 0 ..^ N
2 simpr n = N x = X x = X
3 oveq2 n = N 0 ..^ n = 0 ..^ N
4 3 1 eqtr4di n = N 0 ..^ n = I
5 4 adantr n = N x = X 0 ..^ n = I
6 2 5 oveq12d n = N x = X x 0 ..^ n = X I
7 2 6 oveq12d n = N x = X x x 0 ..^ n = X X I
8 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 |-
9 ovex X X I V
10 7 8 9 ovmpoa Could not format ( ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) : No typesetting found for |- ( ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) with typecode |-
11 10 ex Could not format ( N e. NN0 -> ( X e. _V -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) ) : No typesetting found for |- ( N e. NN0 -> ( X e. _V -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) ) with typecode |-
12 simpr N 0 X V X V
13 df-naryf Could not format -aryF = ( x e. NN0 , n e. _V |-> ( n ^m ( n ^m ( 0 ..^ x ) ) ) ) : No typesetting found for |- -aryF = ( x e. NN0 , n e. _V |-> ( n ^m ( n ^m ( 0 ..^ x ) ) ) ) with typecode |-
14 13 mpondm0 Could not format ( -. ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = (/) ) : No typesetting found for |- ( -. ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = (/) ) with typecode |-
15 12 14 nsyl5 Could not format ( -. X e. _V -> ( N -aryF X ) = (/) ) : No typesetting found for |- ( -. X e. _V -> ( N -aryF X ) = (/) ) with typecode |-
16 simpl X V X I V X V
17 df-map 𝑚 = x V , y V f | f : y x
18 17 mpondm0 ¬ X V X I V X X I =
19 16 18 nsyl5 ¬ X V X X I =
20 15 19 eqtr4d Could not format ( -. X e. _V -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) : No typesetting found for |- ( -. X e. _V -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) with typecode |-
21 11 20 pm2.61d1 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 |-