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=\left(0..^N\right)$$
Assertion	naryfvalelfv	Could not format assertion : No typesetting found for |- ( ( F e. ( N -aryF X ) /\ A : I --> X ) -> ( F ` A ) e. X ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		naryfval.i	$$⊢I=\left(0..^N\right)$$
2	1	naryrcl	Could not format ( F e. ( N -aryF X ) -> ( N e. NN0 /\ X e. _V ) ) : No typesetting found for |- ( F e. ( N -aryF X ) -> ( N e. NN0 /\ X e. _V ) ) with typecode |-
3	1	naryfvalel	Could not format ( ( N e. NN0 /\ X e. _V ) -> ( F e. ( N -aryF X ) <-> F : ( X ^m I ) --> X ) ) : No typesetting found for |- ( ( N e. NN0 /\ X e. _V ) -> ( F e. ( N -aryF X ) <-> F : ( X ^m I ) --> X ) ) with typecode |-
4	3	biimpd	Could not format ( ( N e. NN0 /\ X e. _V ) -> ( F e. ( N -aryF X ) -> F : ( X ^m I ) --> X ) ) : No typesetting found for |- ( ( N e. NN0 /\ X e. _V ) -> ( F e. ( N -aryF X ) -> F : ( X ^m I ) --> X ) ) with typecode |-
5	2 4	mpcom	Could not format ( F e. ( N -aryF X ) -> F : ( X ^m I ) --> X ) : No typesetting found for |- ( F e. ( N -aryF X ) -> F : ( X ^m I ) --> X ) with typecode |-
6	5	adantr	Could not format ( ( F e. ( N -aryF X ) /\ A : I --> X ) -> F : ( X ^m I ) --> X ) : No typesetting found for |- ( ( F e. ( N -aryF X ) /\ A : I --> X ) -> F : ( X ^m I ) --> X ) with typecode |-
7		simpr	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)\to X\in \mathrm{V}$$
8	1	ovexi	$$⊢I\in \mathrm{V}$$
9	8	a1i	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)\to I\in \mathrm{V}$$
10	7 9	elmapd	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)\to \left(A\in \left(X^I\right)\leftrightarrow A:I⟶X\right)$$
11	10	biimpar	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)\wedge A:I⟶X\right)\to A\in \left(X^I\right)$$
12	2 11	sylan	Could not format ( ( F e. ( N -aryF X ) /\ A : I --> X ) -> A e. ( X ^m I ) ) : No typesetting found for |- ( ( F e. ( N -aryF X ) /\ A : I --> X ) -> A e. ( X ^m I ) ) with typecode |-
13	6 12	ffvelrnd	Could not format ( ( F e. ( N -aryF X ) /\ A : I --> X ) -> ( F ` A ) e. X ) : No typesetting found for |- ( ( F e. ( N -aryF X ) /\ A : I --> X ) -> ( F ` A ) e. X ) with typecode |-