MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fsuppres Structured version   Visualization version   GIF version

Theorem fsuppres 9040
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
StepHypRef Expression
1 fsuppres.s . . 3 (𝜑𝐹 finSupp 𝑍)
2 fsuppimp 9021 . . . 4 (𝐹 finSupp 𝑍 → (Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin))
3 relprcnfsupp 9018 . . . . . . . . . . . 12 𝐹 ∈ V → ¬ 𝐹 finSupp 𝑍)
43con4i 114 . . . . . . . . . . 11 (𝐹 finSupp 𝑍𝐹 ∈ V)
51, 4syl 17 . . . . . . . . . 10 (𝜑𝐹 ∈ V)
6 fsuppres.z . . . . . . . . . 10 (𝜑𝑍𝑉)
75, 6jca 515 . . . . . . . . 9 (𝜑 → (𝐹 ∈ V ∧ 𝑍𝑉))
87adantr 484 . . . . . . . 8 ((𝜑 ∧ Fun 𝐹) → (𝐹 ∈ V ∧ 𝑍𝑉))
9 ressuppss 7949 . . . . . . . 8 ((𝐹 ∈ V ∧ 𝑍𝑉) → ((𝐹𝑋) supp 𝑍) ⊆ (𝐹 supp 𝑍))
10 ssfi 8877 . . . . . . . . 9 (((𝐹 supp 𝑍) ∈ Fin ∧ ((𝐹𝑋) supp 𝑍) ⊆ (𝐹 supp 𝑍)) → ((𝐹𝑋) supp 𝑍) ∈ Fin)
1110expcom 417 . . . . . . . 8 (((𝐹𝑋) supp 𝑍) ⊆ (𝐹 supp 𝑍) → ((𝐹 supp 𝑍) ∈ Fin → ((𝐹𝑋) supp 𝑍) ∈ Fin))
128, 9, 113syl 18 . . . . . . 7 ((𝜑 ∧ Fun 𝐹) → ((𝐹 supp 𝑍) ∈ Fin → ((𝐹𝑋) supp 𝑍) ∈ Fin))
1312expcom 417 . . . . . 6 (Fun 𝐹 → (𝜑 → ((𝐹 supp 𝑍) ∈ Fin → ((𝐹𝑋) supp 𝑍) ∈ Fin)))
1413com23 86 . . . . 5 (Fun 𝐹 → ((𝐹 supp 𝑍) ∈ Fin → (𝜑 → ((𝐹𝑋) supp 𝑍) ∈ Fin)))
1514imp 410 . . . 4 ((Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin) → (𝜑 → ((𝐹𝑋) supp 𝑍) ∈ Fin))
162, 15syl 17 . . 3 (𝐹 finSupp 𝑍 → (𝜑 → ((𝐹𝑋) supp 𝑍) ∈ Fin))
171, 16mpcom 38 . 2 (𝜑 → ((𝐹𝑋) supp 𝑍) ∈ Fin)
18 funres 6443 . . . . 5 (Fun 𝐹 → Fun (𝐹𝑋))
1918adantr 484 . . . 4 ((Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin) → Fun (𝐹𝑋))
201, 2, 193syl 18 . . 3 (𝜑 → Fun (𝐹𝑋))
21 resexg 5915 . . . 4 (𝐹 ∈ V → (𝐹𝑋) ∈ V)
221, 4, 213syl 18 . . 3 (𝜑 → (𝐹𝑋) ∈ V)
23 funisfsupp 9020 . . 3 ((Fun (𝐹𝑋) ∧ (𝐹𝑋) ∈ V ∧ 𝑍𝑉) → ((𝐹𝑋) finSupp 𝑍 ↔ ((𝐹𝑋) supp 𝑍) ∈ Fin))
2420, 22, 6, 23syl3anc 1373 . 2 (𝜑 → ((𝐹𝑋) finSupp 𝑍 ↔ ((𝐹𝑋) supp 𝑍) ∈ Fin))
2517, 24mpbird 260 1 (𝜑 → (𝐹𝑋) finSupp 𝑍)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wcel 2112  Vcvv 3423  wss 3883   class class class wbr 5070  cres 5571  Fun wfun 6395  (class class class)co 7235   supp csupp 7927  Fincfn 8650   finSupp cfsupp 9015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5209  ax-nul 5216  ax-pr 5339  ax-un 7545
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-tr 5179  df-id 5472  df-eprel 5478  df-po 5486  df-so 5487  df-fr 5527  df-we 5529  df-xp 5575  df-rel 5576  df-cnv 5577  df-co 5578  df-dm 5579  df-rn 5580  df-res 5581  df-ima 5582  df-ord 6237  df-on 6238  df-lim 6239  df-suc 6240  df-iota 6359  df-fun 6403  df-fn 6404  df-f 6405  df-f1 6406  df-fo 6407  df-f1o 6408  df-fv 6409  df-ov 7238  df-oprab 7239  df-mpo 7240  df-om 7667  df-supp 7928  df-1o 8226  df-en 8651  df-fin 8654  df-fsupp 9016
This theorem is referenced by:  dprdfadd  19440  frlmsplit2  20768  fmptssfisupp  30771  gsumle  31101  zarcmplem  31577  fsuppssind  40041  lindslinindimp2lem3  45520  lindslinindsimp2lem5  45522
  Copyright terms: Public domain W3C validator