Theorem naryfvalixp

Description: The set of the n-ary (endo)functions on a class X expressed with the notation of infinite Cartesian products. (Contributed by AV, 19-May-2024)

	Ref	Expression
Hypothesis	naryfval.i	|- I = ( 0 ..^ N )
Assertion	naryfvalixp	|- ( N e. NN0 -> ( N -aryF X ) = ( X ^m X_ x e. I X ) )

Proof

Step	Hyp	Ref	Expression
1		naryfval.i	|- I = ( 0 ..^ N )
2	1	naryfval	|- ( N e. NN0 -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) )
3	2	adantr	|- ( ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) )
4	1	ovexi	|- I e. _V
5	4	a1i	|- ( N e. NN0 -> I e. _V )
6		ixpconstg	|- ( ( I e. _V /\ X e. _V ) -> X_ x e. I X = ( X ^m I ) )
7	5 6	sylan	|- ( ( N e. NN0 /\ X e. _V ) -> X_ x e. I X = ( X ^m I ) )
8	7	oveq2d	|- ( ( N e. NN0 /\ X e. _V ) -> ( X ^m X_ x e. I X ) = ( X ^m ( X ^m I ) ) )
9	3 8	eqtr4d	|- ( ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = ( X ^m X_ x e. I X ) )
10	9	ex	|- ( N e. NN0 -> ( X e. _V -> ( N -aryF X ) = ( X ^m X_ x e. I X ) ) )
11		simpr	|- ( ( N e. NN0 /\ X e. _V ) -> X e. _V )
12		df-naryf	|- -aryF = ( x e. NN0 , n e. _V |-> ( n ^m ( n ^m ( 0 ..^ x ) ) ) )
13	12	mpondm0	|- ( -. ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = (/) )
14	11 13	nsyl5	|- ( -. X e. _V -> ( N -aryF X ) = (/) )
15		reldmmap	|- Rel dom ^m
16	15	ovprc1	|- ( -. X e. _V -> ( X ^m X_ x e. I X ) = (/) )
17	14 16	eqtr4d	|- ( -. X e. _V -> ( N -aryF X ) = ( X ^m X_ x e. I X ) )
18	10 17	pm2.61d1	|- ( N e. NN0 -> ( N -aryF X ) = ( X ^m X_ x e. I X ) )