naryfvalelfv - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > naryfvalelfv		Structured version Visualization version GIF version

Theorem naryfvalelfv 49297

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

**Hypothesis**
Ref	Expression
naryfval.i	⊢ 𝐼 = (0..^𝑁)

**Assertion**
Ref	Expression
naryfvalelfv	⊢ ((𝐹 ∈ (𝑁-aryF 𝑋) ∧ 𝐴:𝐼⟶𝑋) → (𝐹‘𝐴) ∈ 𝑋)

**Proof of Theorem naryfvalelfv**
Step	Hyp	Ref	Expression
1		naryfval.i	. . . . 5 ⊢ 𝐼 = (0..^𝑁)
2	1	naryrcl 49296	. . . 4 ⊢ (𝐹 ∈ (𝑁-aryF 𝑋) → (𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ V))
3	1	naryfvalel 49295	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ V) → (𝐹 ∈ (𝑁-aryF 𝑋) ↔ 𝐹:(𝑋 ↑_m 𝐼)⟶𝑋))
4	3	biimpd 232	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ V) → (𝐹 ∈ (𝑁-aryF 𝑋) → 𝐹:(𝑋 ↑_m 𝐼)⟶𝑋))
5	2, 4	mpcom 39	. . 3 ⊢ (𝐹 ∈ (𝑁-aryF 𝑋) → 𝐹:(𝑋 ↑_m 𝐼)⟶𝑋)
6	5	adantr 485	. 2 ⊢ ((𝐹 ∈ (𝑁-aryF 𝑋) ∧ 𝐴:𝐼⟶𝑋) → 𝐹:(𝑋 ↑_m 𝐼)⟶𝑋)
7		simpr 489	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ V) → 𝑋 ∈ V)
8	1	ovexi 7445	. . . . . 6 ⊢ 𝐼 ∈ V
9	8	a1i 11	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ V) → 𝐼 ∈ V)
10	7, 9	elmapd 8837	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ V) → (𝐴 ∈ (𝑋 ↑_m 𝐼) ↔ 𝐴:𝐼⟶𝑋))
11	10	biimpar 482	. . 3 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ V) ∧ 𝐴:𝐼⟶𝑋) → 𝐴 ∈ (𝑋 ↑_m 𝐼))
12	2, 11	sylan 591	. 2 ⊢ ((𝐹 ∈ (𝑁-aryF 𝑋) ∧ 𝐴:𝐼⟶𝑋) → 𝐴 ∈ (𝑋 ↑_m 𝐼))
13	6, 12	ffvelcdmd 7081	1 ⊢ ((𝐹 ∈ (𝑁-aryF 𝑋) ∧ 𝐴:𝐼⟶𝑋) → (𝐹‘𝐴) ∈ 𝑋)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1567 ∈ wcel 2149 Vcvv 3463 ⟶wf 6533 ‘cfv 6537 (class class class)co 7411 ↑_m cmap 8824 0cc0 11100 ℕ₀cn0 12504 ..^cfzo 13682 -aryF cnaryf 49291

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-sbc 3754 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-br 5114 df-opab 5178 df-id 5557 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-fv 6545 df-ov 7414 df-oprab 7415 df-mpo 7416 df-map 8826 df-naryf 49292

This theorem is referenced by: (None)

W3C validator