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	|- ( N e. NN0 -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) )

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 ^m ( 0 ..^ n ) ) = ( X ^m I ) )
7	2 6	oveq12d	|- ( ( n = N /\ x = X ) -> ( x ^m ( x ^m ( 0 ..^ n ) ) ) = ( X ^m ( X ^m I ) ) )
8		df-naryf	|- -aryF = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) )
9		ovex	|- ( X ^m ( X ^m I ) ) e. _V
10	7 8 9	ovmpoa	|- ( ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) )
11	10	ex	|- ( N e. NN0 -> ( X e. _V -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) )
12		simpr	|- ( ( N e. NN0 /\ X e. _V ) -> X e. _V )
13		df-naryf	|- -aryF = ( x e. NN0 , n e. _V |-> ( n ^m ( n ^m ( 0 ..^ x ) ) ) )
14	13	mpondm0	|- ( -. ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = (/) )
15	12 14	nsyl5	|- ( -. X e. _V -> ( N -aryF X ) = (/) )
16		simpl	|- ( ( X e. _V /\ ( X ^m I ) e. _V ) -> X e. _V )
17		df-map	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
18	17	mpondm0	|- ( -. ( X e. _V /\ ( X ^m I ) e. _V ) -> ( X ^m ( X ^m I ) ) = (/) )
19	16 18	nsyl5	|- ( -. X e. _V -> ( X ^m ( X ^m I ) ) = (/) )
20	15 19	eqtr4d	|- ( -. X e. _V -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) )
21	11 20	pm2.61d1	|- ( N e. NN0 -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) )