Theorem fsuppres 9363

Description: The restriction of a finitely supported function is finitely supported. (Contributed by AV, 14-Jul-2019.)

Hypotheses

Ref	Expression
fsuppres.s	⊢ (𝜑 → 𝐹 finSupp 𝑍)
fsuppres.z	⊢ (𝜑 → 𝑍 ∈ 𝑉)

Assertion

Ref	Expression
fsuppres	⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍)

Proof of Theorem fsuppres

Step	Hyp	Ref	Expression
1		fsuppres.s	. . 3 ⊢ (𝜑 → 𝐹 finSupp 𝑍)
2		fsuppimp 9338	. . . 4 ⊢ (𝐹 finSupp 𝑍 → (Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin))
3		relprcnfsupp 9334	. . . . . . . . . . . 12 ⊢ (¬ 𝐹 ∈ V → ¬ 𝐹 finSupp 𝑍)
4	3	con4i 115	. . . . . . . . . . 11 ⊢ (𝐹 finSupp 𝑍 → 𝐹 ∈ V)
5	1, 4	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ V)
6		fsuppres.z	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
7	5, 6	jca 521	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∈ V ∧ 𝑍 ∈ 𝑉))
8	7	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ Fun 𝐹) → (𝐹 ∈ V ∧ 𝑍 ∈ 𝑉))
9		ressuppss 8181	. . . . . . . 8 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ 𝑉) → ((𝐹 ↾ 𝑋) supp 𝑍) ⊆ (𝐹 supp 𝑍))
10		ssfi 9167	. . . . . . . . 9 ⊢ (((𝐹 supp 𝑍) ∈ Fin ∧ ((𝐹 ↾ 𝑋) supp 𝑍) ⊆ (𝐹 supp 𝑍)) → ((𝐹 ↾ 𝑋) supp 𝑍) ∈ Fin)
11	10	expcom 419	. . . . . . . 8 ⊢ (((𝐹 ↾ 𝑋) supp 𝑍) ⊆ (𝐹 supp 𝑍) → ((𝐹 supp 𝑍) ∈ Fin → ((𝐹 ↾ 𝑋) supp 𝑍) ∈ Fin))
12	8, 9, 11	3syl 19	. . . . . . 7 ⊢ ((𝜑 ∧ Fun 𝐹) → ((𝐹 supp 𝑍) ∈ Fin → ((𝐹 ↾ 𝑋) supp 𝑍) ∈ Fin))
13	12	expcom 419	. . . . . 6 ⊢ (Fun 𝐹 → (𝜑 → ((𝐹 supp 𝑍) ∈ Fin → ((𝐹 ↾ 𝑋) supp 𝑍) ∈ Fin)))
14	13	com23 87	. . . . 5 ⊢ (Fun 𝐹 → ((𝐹 supp 𝑍) ∈ Fin → (𝜑 → ((𝐹 ↾ 𝑋) supp 𝑍) ∈ Fin)))
15	14	imp 412	. . . 4 ⊢ ((Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin) → (𝜑 → ((𝐹 ↾ 𝑋) supp 𝑍) ∈ Fin))
16	2, 15	syl 18	. . 3 ⊢ (𝐹 finSupp 𝑍 → (𝜑 → ((𝐹 ↾ 𝑋) supp 𝑍) ∈ Fin))
17	1, 16	mpcom 39	. 2 ⊢ (𝜑 → ((𝐹 ↾ 𝑋) supp 𝑍) ∈ Fin)
18		funres 6575	. . . . 5 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝑋))
19	18	adantr 486	. . . 4 ⊢ ((Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin) → Fun (𝐹 ↾ 𝑋))
20	1, 2, 19	3syl 19	. . 3 ⊢ (𝜑 → Fun (𝐹 ↾ 𝑋))
21		resexg 6020	. . . 4 ⊢ (𝐹 ∈ V → (𝐹 ↾ 𝑋) ∈ V)
22	1, 4, 21	3syl 19	. . 3 ⊢ (𝜑 → (𝐹 ↾ 𝑋) ∈ V)
23		funisfsupp 9337	. . 3 ⊢ ((Fun (𝐹 ↾ 𝑋) ∧ (𝐹 ↾ 𝑋) ∈ V ∧ 𝑍 ∈ 𝑉) → ((𝐹 ↾ 𝑋) finSupp 𝑍 ↔ ((𝐹 ↾ 𝑋) supp 𝑍) ∈ Fin))
24	20, 22, 6, 23	syl3anc 1398	. 2 ⊢ (𝜑 → ((𝐹 ↾ 𝑋) finSupp 𝑍 ↔ ((𝐹 ↾ 𝑋) supp 𝑍) ∈ Fin))
25	17, 24	mpbird 260	1 ⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  Vcvv 3450   ⊆ wss 3899   class class class wbr 5103   ↾ cres 5657  Fun wfun 6527  (class class class)co 7413   supp csupp 8158  Fincfn 8952   finSupp cfsupp 9331

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-supp 8159  df-1o 8455  df-en 8953  df-fin 8956  df-fsupp 9332

This theorem is used by:  fmptssfisupp  9364  dprdfadd  20149  gsumle  20272  frlmsplit2  21986  psrbagres  22145  elrspunsn  33857  rprmdvdsprod  33944  selvply1rhm0  34036  extvfvvcl  34045  extvfvcl  34046  evlextv  34052  esplyind  34085  zarcmplem  34391  evlselv  43435  fsuppssind  43439  cantnf2  44166  lindslinindimp2lem3  49390  lindslinindsimp2lem5  49392