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=\left(0..^N\right)$$
Assertion	naryfvalixp	$$⊢N\in {\mathbb{N}}_0\to N\mathrm{-aryF}X=X^{\underset{x\in I}{⨉}X}$$

Proof

Step	Hyp	Ref	Expression
1		naryfval.i	$$⊢I=\left(0..^N\right)$$
2	1	naryfval	$$⊢N\in {\mathbb{N}}_0\to N\mathrm{-aryF}X=X^{\left(X^I\right)}$$
3	2	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)\to N\mathrm{-aryF}X=X^{\left(X^I\right)}$$
4	1	ovexi	$$⊢I\in \mathrm{V}$$
5	4	a1i	$$⊢N\in {\mathbb{N}}_0\to I\in \mathrm{V}$$
6		ixpconstg	$$⊢\left(I\in \mathrm{V}\wedge X\in \mathrm{V}\right)\to \underset{x\in I}{⨉}X=X^I$$
7	5 6	sylan	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)\to \underset{x\in I}{⨉}X=X^I$$
8	7	oveq2d	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)\to X^{\underset{x\in I}{⨉}X}=X^{\left(X^I\right)}$$
9	3 8	eqtr4d	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)\to N\mathrm{-aryF}X=X^{\underset{x\in I}{⨉}X}$$
10	9	ex	$$⊢N\in {\mathbb{N}}_0\to \left(X\in \mathrm{V}\to N\mathrm{-aryF}X=X^{\underset{x\in I}{⨉}X}\right)$$
11		simpr	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)\to X\in \mathrm{V}$$
12		df-naryf	$$⊢\mathrm{-aryF}=\left(x\in {\mathbb{N}}_0,n\in \mathrm{V}⟼n^{\left(n^{\left(0..^x\right)}\right)}\right)$$
13	12	mpondm0	$$⊢\neg \left(N\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)\to N\mathrm{-aryF}X=\varnothing$$
14	11 13	nsyl5	$$⊢\neg X\in \mathrm{V}\to N\mathrm{-aryF}X=\varnothing$$
15		reldmmap	$$⊢\mathrm{Rel}\mathrm{dom}{\uparrow }_{𝑚}$$
16	15	ovprc1	$$⊢\neg X\in \mathrm{V}\to X^{\underset{x\in I}{⨉}X}=\varnothing$$
17	14 16	eqtr4d	$$⊢\neg X\in \mathrm{V}\to N\mathrm{-aryF}X=X^{\underset{x\in I}{⨉}X}$$
18	10 17	pm2.61d1	$$⊢N\in {\mathbb{N}}_0\to N\mathrm{-aryF}X=X^{\underset{x\in I}{⨉}X}$$