Theorem naryfvalelfv

Description: The value of an n-ary (endo)function on a set X is an element of X . (Contributed by AV, 14-May-2024)

	Ref	Expression
Hypothesis	naryfval.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
Assertion	naryfvalelfv	⊢ ( ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) ∧ 𝐴 : 𝐼 ⟶ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		naryfval.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
2	1	naryrcl	⊢ ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) )
3	1	naryfvalel	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) → ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋 ↑m 𝐼 ) ⟶ 𝑋 ) )
4	3	biimpd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) → ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) → 𝐹 : ( 𝑋 ↑m 𝐼 ) ⟶ 𝑋 ) )
5	2 4	mpcom	⊢ ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) → 𝐹 : ( 𝑋 ↑m 𝐼 ) ⟶ 𝑋 )
6	5	adantr	⊢ ( ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) ∧ 𝐴 : 𝐼 ⟶ 𝑋 ) → 𝐹 : ( 𝑋 ↑m 𝐼 ) ⟶ 𝑋 )
7		simpr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) → 𝑋 ∈ V )
8	1	ovexi	⊢ 𝐼 ∈ V
9	8	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) → 𝐼 ∈ V )
10	7 9	elmapd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) → ( 𝐴 ∈ ( 𝑋 ↑m 𝐼 ) ↔ 𝐴 : 𝐼 ⟶ 𝑋 ) )
11	10	biimpar	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V ) ∧ 𝐴 : 𝐼 ⟶ 𝑋 ) → 𝐴 ∈ ( 𝑋 ↑m 𝐼 ) )
12	2 11	sylan	⊢ ( ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) ∧ 𝐴 : 𝐼 ⟶ 𝑋 ) → 𝐴 ∈ ( 𝑋 ↑m 𝐼 ) )
13	6 12	ffvelcdmd	⊢ ( ( 𝐹 ∈ ( 𝑁 -aryF 𝑋 ) ∧ 𝐴 : 𝐼 ⟶ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝑋 )