Theorem naryfvalel

Description: An n-ary (endo)function on a set X . (Contributed by AV, 14-May-2024)

	Ref	Expression
Hypothesis	naryfval.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
Assertion	naryfvalel	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋 ↑m 𝐼 ) ⟶ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		naryfval.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
2	1	naryfval	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 -aryF 𝑋 ) = ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) )
3	2	eleq2d	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) ↔ 𝐹 ∈ ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) ) )
4		ovex	⊢ ( 𝑋 ↑m 𝐼 ) ∈ V
5		elmapg	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑋 ↑m 𝐼 ) ∈ V ) → ( 𝐹 ∈ ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) ↔ 𝐹 : ( 𝑋 ↑m 𝐼 ) ⟶ 𝑋 ) )
6	4 5	mpan2	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 ∈ ( 𝑋 ↑m ( 𝑋 ↑m 𝐼 ) ) ↔ 𝐹 : ( 𝑋 ↑m 𝐼 ) ⟶ 𝑋 ) )
7	3 6	sylan9bb	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋 ↑m 𝐼 ) ⟶ 𝑋 ) )