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 \in ℕ_{0} \to N -aryF X = X^{(X^{I})}$

Step	Hyp	Ref	Expression
1		naryfval.i	$⊢ I = (0 ..^N)$
2		simpr	$⊢ (n = N \land x = X) \to x = X$
3		oveq2	$⊢ n = N \to (0 ..^n) = (0 ..^N)$
4	3 1	eqtr4di	$⊢ n = N \to (0 ..^n) = I$
5	4	adantr	$⊢ (n = N \land x = X) \to (0 ..^n) = I$
6	2 5	oveq12d	$⊢ (n = N \land x = X) \to x^{(0 ..^n)} = X^{I}$
7	2 6	oveq12d	$⊢ (n = N \land x = X) \to x^{(x^{(0 ..^n)})} = X^{(X^{I})}$
8		df-naryf	$⊢ -aryF = (n \in ℕ_{0}, x \in V ⟼ x^{(x^{(0 ..^n)})})$
9		ovex	$⊢ X^{(X^{I})} \in V$
10	7 8 9	ovmpoa	$⊢ (N \in ℕ_{0} \land X \in V) \to N -aryF X = X^{(X^{I})}$
11	10	ex	$⊢ N \in ℕ_{0} \to (X \in V \to N -aryF X = X^{(X^{I})})$
12		simpr	$⊢ (N \in ℕ_{0} \land X \in V) \to X \in V$
13		df-naryf	$⊢ -aryF = (x \in ℕ_{0}, n \in V ⟼ n^{(n^{(0 ..^x)})})$
14	13	mpondm0	$⊢ \neg (N \in ℕ_{0} \land X \in V) \to N -aryF X = \emptyset$
15	12 14	nsyl5	$⊢ \neg X \in V \to N -aryF X = \emptyset$
16		simpl	$⊢ (X \in V \land X^{I} \in V) \to X \in V$
17		df-map	$⊢ ↑_{𝑚} = (x \in V, y \in V ⟼ \{f \| f : y ⟶ x\})$
18	17	mpondm0	$⊢ \neg (X \in V \land X^{I} \in V) \to X^{(X^{I})} = \emptyset$
19	16 18	nsyl5	$⊢ \neg X \in V \to X^{(X^{I})} = \emptyset$
20	15 19	eqtr4d	$⊢ \neg X \in V \to N -aryF X = X^{(X^{I})}$
21	11 20	pm2.61d1	$⊢ N \in ℕ_{0} \to N -aryF X = X^{(X^{I})}$

Metamath Proof Explorer