Theorem naryrcl

Description: Reverse closure for n-ary (endo)functions. (Contributed by AV, 14-May-2024)

	Ref	Expression
Hypothesis	naryfval.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
Assertion	naryrcl	⊢ ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		naryfval.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
2		df-naryf	⊢ -aryF = ( 𝑥 ∈ ℕ0 , 𝑛 ∈ V ↦ ( 𝑛 ↑m ( 𝑛 ↑m ( 0 ..^ 𝑥 ) ) ) )
3	2	elmpocl	⊢ ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) )