Metamath Proof Explorer

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 ⊢ I = 0 ..^ N
Assertion naryfvalelfv ⊢ F ∈ N -aryF X ∧ A : I ⟶ X → F ⁡ A ∈ X

Proof

Step Hyp Ref Expression
1 naryfval.i ⊢ I = 0 ..^ N
2 1 naryrcl ⊢ F ∈ N -aryF X → N ∈ ℕ 0 ∧ X ∈ V
3 1 naryfvalel ⊢ N ∈ ℕ 0 ∧ X ∈ V → F ∈ N -aryF X ↔ F : X I ⟶ X
4 3 biimpd ⊢ N ∈ ℕ 0 ∧ X ∈ V → F ∈ N -aryF X → F : X I ⟶ X
5 2 4 mpcom ⊢ F ∈ N -aryF X → F : X I ⟶ X
6 5 adantr ⊢ F ∈ N -aryF X ∧ A : I ⟶ X → F : X I ⟶ X
7 simpr ⊢ N ∈ ℕ 0 ∧ X ∈ V → X ∈ V
8 1 ovexi ⊢ I ∈ V
9 8 a1i ⊢ N ∈ ℕ 0 ∧ X ∈ V → I ∈ V
10 7 9 elmapd ⊢ N ∈ ℕ 0 ∧ X ∈ V → A ∈ X I ↔ A : I ⟶ X
11 10 biimpar ⊢ N ∈ ℕ 0 ∧ X ∈ V ∧ A : I ⟶ X → A ∈ X I
12 2 11 sylan ⊢ F ∈ N -aryF X ∧ A : I ⟶ X → A ∈ X I
13 6 12 ffvelcdmd ⊢ F ∈ N -aryF X ∧ A : I ⟶ X → F ⁡ A ∈ X