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	⊢ 𝐼 = ( 0 ..^ 𝑁 )
Assertion	naryfval	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 -aryF 𝑋 ) = ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) )

Proof

Step	Hyp	Ref	Expression
1		naryfval.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
2		simpr	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
3		oveq2	⊢ ( 𝑛 = 𝑁 → ( 0 ..^ 𝑛 ) = ( 0 ..^ 𝑁 ) )
4	3 1	eqtr4di	⊢ ( 𝑛 = 𝑁 → ( 0 ..^ 𝑛 ) = 𝐼 )
5	4	adantr	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ( 0 ..^ 𝑛 ) = 𝐼 )
6	2 5	oveq12d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ( 𝑥 ↑m ( 0 ..^ 𝑛 ) ) = ( 𝑋 ↑m 𝐼 ) )
7	2 6	oveq12d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ( 𝑥 ↑m ( 𝑥 ↑m ( 0 ..^ 𝑛 ) ) ) = ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) )
8		df-naryf	⊢ -aryF = ( 𝑛 ∈ ℕ0 , 𝑥 ∈ V ↦ ( 𝑥 ↑m ( 𝑥 ↑m ( 0 ..^ 𝑛 ) ) ) )
9		ovex	⊢ ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) ∈ V
10	7 8 9	ovmpoa	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) → ( 𝑁 -aryF 𝑋 ) = ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) )
11	10	ex	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑋 ∈ V → ( 𝑁 -aryF 𝑋 ) = ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) ) )
12		simpr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) → 𝑋 ∈ V )
13		df-naryf	⊢ -aryF = ( 𝑥 ∈ ℕ0 , 𝑛 ∈ V ↦ ( 𝑛 ↑m ( 𝑛 ↑m ( 0 ..^ 𝑥 ) ) ) )
14	13	mpondm0	⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) → ( 𝑁 -aryF 𝑋 ) = ∅ )
15	12 14	nsyl5	⊢ ( ¬ 𝑋 ∈ V → ( 𝑁 -aryF 𝑋 ) = ∅ )
16		simpl	⊢ ( ( 𝑋 ∈ V ∧ ( 𝑋 ↑m 𝐼 ) ∈ V ) → 𝑋 ∈ V )
17		df-map	⊢ ↑m = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑓 ∣ 𝑓 : 𝑦 ⟶ 𝑥 } )
18	17	mpondm0	⊢ ( ¬ ( 𝑋 ∈ V ∧ ( 𝑋 ↑m 𝐼 ) ∈ V ) → ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) = ∅ )
19	16 18	nsyl5	⊢ ( ¬ 𝑋 ∈ V → ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) = ∅ )
20	15 19	eqtr4d	⊢ ( ¬ 𝑋 ∈ V → ( 𝑁 -aryF 𝑋 ) = ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) )
21	11 20	pm2.61d1	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 -aryF 𝑋 ) = ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) )