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

Theorem fsuppunbi 9387
Description: If the union of two classes/functions is a function, this union is finitely supported iff the two functions are finitely supported. (Contributed by AV, 18-Jun-2019.)
Hypothesis
Ref Expression
fsuppunbi.u (𝜑 → Fun (𝐹𝐺))
Assertion
Ref Expression
fsuppunbi (𝜑 → ((𝐹𝐺) finSupp 𝑍 ↔ (𝐹 finSupp 𝑍𝐺 finSupp 𝑍)))

Proof of Theorem fsuppunbi
StepHypRef Expression
1 relfsupp 9366 . . . . 5 Rel finSupp
21brrelex12i 5732 . . . 4 ((𝐹𝐺) finSupp 𝑍 → ((𝐹𝐺) ∈ V ∧ 𝑍 ∈ V))
3 unexb 7738 . . . . 5 ((𝐹 ∈ V ∧ 𝐺 ∈ V) ↔ (𝐹𝐺) ∈ V)
4 simpr 484 . . . . . . . . . . . 12 ((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) → ((𝐹𝐺) supp 𝑍) ∈ Fin)
54adantr 480 . . . . . . . . . . 11 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → ((𝐹𝐺) supp 𝑍) ∈ Fin)
6 simprlr 777 . . . . . . . . . . . 12 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝐺 ∈ V)
76suppun 8172 . . . . . . . . . . 11 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐹 supp 𝑍) ⊆ ((𝐹𝐺) supp 𝑍))
85, 7ssfid 9270 . . . . . . . . . 10 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐹 supp 𝑍) ∈ Fin)
9 fununfun 6597 . . . . . . . . . . . . . 14 (Fun (𝐹𝐺) → (Fun 𝐹 ∧ Fun 𝐺))
109simpld 494 . . . . . . . . . . . . 13 (Fun (𝐹𝐺) → Fun 𝐹)
1110adantr 480 . . . . . . . . . . . 12 ((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) → Fun 𝐹)
1211adantr 480 . . . . . . . . . . 11 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → Fun 𝐹)
13 simprll 776 . . . . . . . . . . 11 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝐹 ∈ V)
14 simpr 484 . . . . . . . . . . . 12 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V) → 𝑍 ∈ V)
1514adantl 481 . . . . . . . . . . 11 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝑍 ∈ V)
16 funisfsupp 9370 . . . . . . . . . . 11 ((Fun 𝐹𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 finSupp 𝑍 ↔ (𝐹 supp 𝑍) ∈ Fin))
1712, 13, 15, 16syl3anc 1370 . . . . . . . . . 10 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐹 finSupp 𝑍 ↔ (𝐹 supp 𝑍) ∈ Fin))
188, 17mpbird 256 . . . . . . . . 9 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝐹 finSupp 𝑍)
19 uncom 4154 . . . . . . . . . . . . . . . 16 (𝐹𝐺) = (𝐺𝐹)
2019oveq1i 7422 . . . . . . . . . . . . . . 15 ((𝐹𝐺) supp 𝑍) = ((𝐺𝐹) supp 𝑍)
2120eleq1i 2823 . . . . . . . . . . . . . 14 (((𝐹𝐺) supp 𝑍) ∈ Fin ↔ ((𝐺𝐹) supp 𝑍) ∈ Fin)
2221biimpi 215 . . . . . . . . . . . . 13 (((𝐹𝐺) supp 𝑍) ∈ Fin → ((𝐺𝐹) supp 𝑍) ∈ Fin)
2322adantl 481 . . . . . . . . . . . 12 ((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) → ((𝐺𝐹) supp 𝑍) ∈ Fin)
2423adantr 480 . . . . . . . . . . 11 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → ((𝐺𝐹) supp 𝑍) ∈ Fin)
2513suppun 8172 . . . . . . . . . . 11 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐺 supp 𝑍) ⊆ ((𝐺𝐹) supp 𝑍))
2624, 25ssfid 9270 . . . . . . . . . 10 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐺 supp 𝑍) ∈ Fin)
279simprd 495 . . . . . . . . . . . . 13 (Fun (𝐹𝐺) → Fun 𝐺)
2827adantr 480 . . . . . . . . . . . 12 ((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) → Fun 𝐺)
2928adantr 480 . . . . . . . . . . 11 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → Fun 𝐺)
30 funisfsupp 9370 . . . . . . . . . . 11 ((Fun 𝐺𝐺 ∈ V ∧ 𝑍 ∈ V) → (𝐺 finSupp 𝑍 ↔ (𝐺 supp 𝑍) ∈ Fin))
3129, 6, 15, 30syl3anc 1370 . . . . . . . . . 10 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐺 finSupp 𝑍 ↔ (𝐺 supp 𝑍) ∈ Fin))
3226, 31mpbird 256 . . . . . . . . 9 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝐺 finSupp 𝑍)
3318, 32jca 511 . . . . . . . 8 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐹 finSupp 𝑍𝐺 finSupp 𝑍))
3433a1d 25 . . . . . . 7 (((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝜑 → (𝐹 finSupp 𝑍𝐺 finSupp 𝑍)))
3534ex 412 . . . . . 6 ((Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin) → (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V) → (𝜑 → (𝐹 finSupp 𝑍𝐺 finSupp 𝑍))))
36 fsuppimp 9371 . . . . . 6 ((𝐹𝐺) finSupp 𝑍 → (Fun (𝐹𝐺) ∧ ((𝐹𝐺) supp 𝑍) ∈ Fin))
3735, 36syl11 33 . . . . 5 (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V) → ((𝐹𝐺) finSupp 𝑍 → (𝜑 → (𝐹 finSupp 𝑍𝐺 finSupp 𝑍))))
383, 37sylanbr 581 . . . 4 (((𝐹𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹𝐺) finSupp 𝑍 → (𝜑 → (𝐹 finSupp 𝑍𝐺 finSupp 𝑍))))
392, 38mpcom 38 . . 3 ((𝐹𝐺) finSupp 𝑍 → (𝜑 → (𝐹 finSupp 𝑍𝐺 finSupp 𝑍)))
4039com12 32 . 2 (𝜑 → ((𝐹𝐺) finSupp 𝑍 → (𝐹 finSupp 𝑍𝐺 finSupp 𝑍)))
41 simpl 482 . . . . . 6 ((𝐹 finSupp 𝑍𝐺 finSupp 𝑍) → 𝐹 finSupp 𝑍)
42 simpr 484 . . . . . 6 ((𝐹 finSupp 𝑍𝐺 finSupp 𝑍) → 𝐺 finSupp 𝑍)
4341, 42fsuppun 9385 . . . . 5 ((𝐹 finSupp 𝑍𝐺 finSupp 𝑍) → ((𝐹𝐺) supp 𝑍) ∈ Fin)
4443adantl 481 . . . 4 ((𝜑 ∧ (𝐹 finSupp 𝑍𝐺 finSupp 𝑍)) → ((𝐹𝐺) supp 𝑍) ∈ Fin)
45 fsuppunbi.u . . . . . 6 (𝜑 → Fun (𝐹𝐺))
4645adantr 480 . . . . 5 ((𝜑 ∧ (𝐹 finSupp 𝑍𝐺 finSupp 𝑍)) → Fun (𝐹𝐺))
471brrelex1i 5733 . . . . . . 7 (𝐹 finSupp 𝑍𝐹 ∈ V)
481brrelex1i 5733 . . . . . . 7 (𝐺 finSupp 𝑍𝐺 ∈ V)
49 unexg 7739 . . . . . . 7 ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹𝐺) ∈ V)
5047, 48, 49syl2an 595 . . . . . 6 ((𝐹 finSupp 𝑍𝐺 finSupp 𝑍) → (𝐹𝐺) ∈ V)
5150adantl 481 . . . . 5 ((𝜑 ∧ (𝐹 finSupp 𝑍𝐺 finSupp 𝑍)) → (𝐹𝐺) ∈ V)
521brrelex2i 5734 . . . . . . 7 (𝐹 finSupp 𝑍𝑍 ∈ V)
5352adantr 480 . . . . . 6 ((𝐹 finSupp 𝑍𝐺 finSupp 𝑍) → 𝑍 ∈ V)
5453adantl 481 . . . . 5 ((𝜑 ∧ (𝐹 finSupp 𝑍𝐺 finSupp 𝑍)) → 𝑍 ∈ V)
55 funisfsupp 9370 . . . . 5 ((Fun (𝐹𝐺) ∧ (𝐹𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹𝐺) finSupp 𝑍 ↔ ((𝐹𝐺) supp 𝑍) ∈ Fin))
5646, 51, 54, 55syl3anc 1370 . . . 4 ((𝜑 ∧ (𝐹 finSupp 𝑍𝐺 finSupp 𝑍)) → ((𝐹𝐺) finSupp 𝑍 ↔ ((𝐹𝐺) supp 𝑍) ∈ Fin))
5744, 56mpbird 256 . . 3 ((𝜑 ∧ (𝐹 finSupp 𝑍𝐺 finSupp 𝑍)) → (𝐹𝐺) finSupp 𝑍)
5857ex 412 . 2 (𝜑 → ((𝐹 finSupp 𝑍𝐺 finSupp 𝑍) → (𝐹𝐺) finSupp 𝑍))
5940, 58impbid 211 1 (𝜑 → ((𝐹𝐺) finSupp 𝑍 ↔ (𝐹 finSupp 𝑍𝐺 finSupp 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wcel 2105  Vcvv 3473  cun 3947   class class class wbr 5149  Fun wfun 6538  (class class class)co 7412   supp csupp 8149  Fincfn 8942   finSupp cfsupp 9364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7728
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7859  df-supp 8150  df-1o 8469  df-en 8943  df-fin 8946  df-fsupp 9365
This theorem is referenced by:  funsnfsupp  9390  lbsdiflsp0  32996
  Copyright terms: Public domain W3C validator