Theorem finnzfsuppd 41273

Description: If a function is zero outside of a finite set, it has finite support. (Contributed by Rohan Ridenour, 13-May-2024.)

Hypotheses

Ref	Expression
finnzfsuppd.1	⊢ (𝜑 → 𝐹 ∈ 𝑉)
finnzfsuppd.2	⊢ (𝜑 → 𝐹 Fn 𝐷)
finnzfsuppd.3	⊢ (𝜑 → 𝑍 ∈ 𝑈)
finnzfsuppd.4	⊢ (𝜑 → 𝐴 ∈ Fin)
finnzfsuppd.5	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ 𝐴 ∨ (𝐹‘𝑥) = 𝑍))

Assertion

Ref	Expression
finnzfsuppd	⊢ (𝜑 → 𝐹 finSupp 𝑍)

Distinct variable groups:   𝜑,𝑥   𝑥,𝐴   𝑥,𝐹   𝑥,𝑍

Allowed substitution hints:   𝐷(𝑥)   𝑈(𝑥)   𝑉(𝑥)

Proof of Theorem finnzfsuppd

Step	Hyp	Ref	Expression
1		finnzfsuppd.4	. . 3 ⊢ (𝜑 → 𝐴 ∈ Fin)
2		finnzfsuppd.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 Fn 𝐷)
3		finnzfsuppd.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ 𝑉)
4	3, 2	fndmexd 7609	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ V)
5		finnzfsuppd.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝑈)
6		elsuppfn 7838	. . . . . . . . . 10 ⊢ ((𝐹 Fn 𝐷 ∧ 𝐷 ∈ V ∧ 𝑍 ∈ 𝑈) → (𝑥 ∈ (𝐹 supp 𝑍) ↔ (𝑥 ∈ 𝐷 ∧ (𝐹‘𝑥) ≠ 𝑍)))
7	2, 4, 5, 6	syl3anc 1369	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐹 supp 𝑍) ↔ (𝑥 ∈ 𝐷 ∧ (𝐹‘𝑥) ≠ 𝑍)))
8	7	biimpa 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 𝑍)) → (𝑥 ∈ 𝐷 ∧ (𝐹‘𝑥) ≠ 𝑍))
9	8	simpld 499	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 𝑍)) → 𝑥 ∈ 𝐷)
10		finnzfsuppd.5	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ 𝐴 ∨ (𝐹‘𝑥) = 𝑍))
11	9, 10	syldan 595	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 𝑍)) → (𝑥 ∈ 𝐴 ∨ (𝐹‘𝑥) = 𝑍))
12	8	simprd 500	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 𝑍)) → (𝐹‘𝑥) ≠ 𝑍)
13	12	neneqd 2954	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 𝑍)) → ¬ (𝐹‘𝑥) = 𝑍)
14	11, 13	olcnd 875	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 𝑍)) → 𝑥 ∈ 𝐴)
15	14	ex 417	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (𝐹 supp 𝑍) → 𝑥 ∈ 𝐴))
16	15	ssrdv 3894	. . 3 ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝐴)
17	1, 16	ssfid 8755	. 2 ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
18		fnfun 6427	. . . 4 ⊢ (𝐹 Fn 𝐷 → Fun 𝐹)
19	2, 18	syl 17	. . 3 ⊢ (𝜑 → Fun 𝐹)
20		funisfsupp 8856	. . 3 ⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑈) → (𝐹 finSupp 𝑍 ↔ (𝐹 supp 𝑍) ∈ Fin))
21	19, 3, 5, 20	syl3anc 1369	. 2 ⊢ (𝜑 → (𝐹 finSupp 𝑍 ↔ (𝐹 supp 𝑍) ∈ Fin))
22	17, 21	mpbird 260	1 ⊢ (𝜑 → 𝐹 finSupp 𝑍)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 845   = wceq 1539   ∈ wcel 2112   ≠ wne 2949  Vcvv 3407   class class class wbr 5025  Fun wfun 6322   Fn wfn 6323  ‘cfv 6328  (class class class)co 7143   supp csupp 7828  Fincfn 8520   finSupp cfsupp 8851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5149  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-ral 3073  df-rex 3074  df-reu 3075  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-pss 3873  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-tp 4520  df-op 4522  df-uni 4792  df-iun 4878  df-br 5026  df-opab 5088  df-mpt 5106  df-tr 5132  df-id 5423  df-eprel 5428  df-po 5436  df-so 5437  df-fr 5476  df-we 5478  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7146  df-oprab 7147  df-mpo 7148  df-om 7573  df-supp 7829  df-er 8292  df-en 8521  df-fin 8524  df-fsupp 8852

This theorem is referenced by:  mnringmulrcld  41294