# Metamath Proof Explorer

## Theorem sge0resplit

Description: sum^ splits into two parts, when it's a real number. This is a special case of sge0split . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0resplit.a ${⊢}{\phi }\to {A}\in {V}$
sge0resplit.b ${⊢}{\phi }\to {B}\in {W}$
sge0resplit.u ${⊢}{U}={A}\cup {B}$
sge0resplit.in0 ${⊢}{\phi }\to {A}\cap {B}=\varnothing$
sge0resplit.f ${⊢}{\phi }\to {F}:{U}⟶\left[0,\mathrm{+\infty }\right]$
sge0resplit.re ${⊢}{\phi }\to \mathrm{sum^}\left({F}\right)\in ℝ$
Assertion sge0resplit ${⊢}{\phi }\to \mathrm{sum^}\left({F}\right)=\mathrm{sum^}\left({{F}↾}_{{A}}\right)+\mathrm{sum^}\left({{F}↾}_{{B}}\right)$

### Proof

Step Hyp Ref Expression
1 sge0resplit.a ${⊢}{\phi }\to {A}\in {V}$
2 sge0resplit.b ${⊢}{\phi }\to {B}\in {W}$
3 sge0resplit.u ${⊢}{U}={A}\cup {B}$
4 sge0resplit.in0 ${⊢}{\phi }\to {A}\cap {B}=\varnothing$
5 sge0resplit.f ${⊢}{\phi }\to {F}:{U}⟶\left[0,\mathrm{+\infty }\right]$
6 sge0resplit.re ${⊢}{\phi }\to \mathrm{sum^}\left({F}\right)\in ℝ$
7 ssun1 ${⊢}{A}\subseteq {A}\cup {B}$
8 3 eqcomi ${⊢}{A}\cup {B}={U}$
9 7 8 sseqtri ${⊢}{A}\subseteq {U}$
10 9 a1i ${⊢}{\phi }\to {A}\subseteq {U}$
11 5 10 fssresd ${⊢}{\phi }\to \left({{F}↾}_{{A}}\right):{A}⟶\left[0,\mathrm{+\infty }\right]$
12 3 a1i ${⊢}{\phi }\to {U}={A}\cup {B}$
13 unexg ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to {A}\cup {B}\in \mathrm{V}$
14 1 2 13 syl2anc ${⊢}{\phi }\to {A}\cup {B}\in \mathrm{V}$
15 12 14 eqeltrd ${⊢}{\phi }\to {U}\in \mathrm{V}$
16 15 5 6 sge0ssre ${⊢}{\phi }\to \mathrm{sum^}\left({{F}↾}_{{A}}\right)\in ℝ$
17 1 11 16 sge0supre ${⊢}{\phi }\to \mathrm{sum^}\left({{F}↾}_{{A}}\right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),ℝ,<\right)$
18 17 16 eqeltrrd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),ℝ,<\right)\in ℝ$
19 ssun2 ${⊢}{B}\subseteq {A}\cup {B}$
20 19 8 sseqtri ${⊢}{B}\subseteq {U}$
21 20 a1i ${⊢}{\phi }\to {B}\subseteq {U}$
22 5 21 fssresd ${⊢}{\phi }\to \left({{F}↾}_{{B}}\right):{B}⟶\left[0,\mathrm{+\infty }\right]$
23 15 5 6 sge0ssre ${⊢}{\phi }\to \mathrm{sum^}\left({{F}↾}_{{B}}\right)\in ℝ$
24 2 22 23 sge0supre ${⊢}{\phi }\to \mathrm{sum^}\left({{F}↾}_{{B}}\right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),ℝ,<\right)$
25 24 23 eqeltrrd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),ℝ,<\right)\in ℝ$
26 rexadd ${⊢}\left(sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),ℝ,<\right)\in ℝ\wedge sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),ℝ,<\right)\in ℝ\right)\to sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),ℝ,<\right){+}_{𝑒}sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),ℝ,<\right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),ℝ,<\right)+sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),ℝ,<\right)$
27 18 25 26 syl2anc ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),ℝ,<\right){+}_{𝑒}sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),ℝ,<\right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),ℝ,<\right)+sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),ℝ,<\right)$
28 15 5 6 sge0rern ${⊢}{\phi }\to ¬\mathrm{+\infty }\in \mathrm{ran}{F}$
29 nelrnres ${⊢}¬\mathrm{+\infty }\in \mathrm{ran}{F}\to ¬\mathrm{+\infty }\in \mathrm{ran}\left({{F}↾}_{{A}}\right)$
30 28 29 syl ${⊢}{\phi }\to ¬\mathrm{+\infty }\in \mathrm{ran}\left({{F}↾}_{{A}}\right)$
31 11 30 fge0iccico ${⊢}{\phi }\to \left({{F}↾}_{{A}}\right):{A}⟶\left[0,\mathrm{+\infty }\right)$
32 31 sge0rnre ${⊢}{\phi }\to \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\subseteq ℝ$
33 sge0rnn0 ${⊢}\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\ne \varnothing$
34 33 a1i ${⊢}{\phi }\to \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\ne \varnothing$
35 1 31 sge0reval ${⊢}{\phi }\to \mathrm{sum^}\left({{F}↾}_{{A}}\right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),{ℝ}^{*},<\right)$
36 35 eqcomd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),{ℝ}^{*},<\right)=\mathrm{sum^}\left({{F}↾}_{{A}}\right)$
37 36 16 eqeltrd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),{ℝ}^{*},<\right)\in ℝ$
38 supxrre3 ${⊢}\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\subseteq ℝ\wedge \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\ne \varnothing \right)\to \left(sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),{ℝ}^{*},<\right)\in ℝ↔\exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{t}\le {w}\right)$
39 32 34 38 syl2anc ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),{ℝ}^{*},<\right)\in ℝ↔\exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{t}\le {w}\right)$
40 37 39 mpbid ${⊢}{\phi }\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{t}\le {w}$
41 nelrnres ${⊢}¬\mathrm{+\infty }\in \mathrm{ran}{F}\to ¬\mathrm{+\infty }\in \mathrm{ran}\left({{F}↾}_{{B}}\right)$
42 28 41 syl ${⊢}{\phi }\to ¬\mathrm{+\infty }\in \mathrm{ran}\left({{F}↾}_{{B}}\right)$
43 22 42 fge0iccico ${⊢}{\phi }\to \left({{F}↾}_{{B}}\right):{B}⟶\left[0,\mathrm{+\infty }\right)$
44 43 sge0rnre ${⊢}{\phi }\to \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\subseteq ℝ$
45 sge0rnn0 ${⊢}\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\ne \varnothing$
46 45 a1i ${⊢}{\phi }\to \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\ne \varnothing$
47 2 43 sge0reval ${⊢}{\phi }\to \mathrm{sum^}\left({{F}↾}_{{B}}\right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),{ℝ}^{*},<\right)$
48 47 eqcomd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),{ℝ}^{*},<\right)=\mathrm{sum^}\left({{F}↾}_{{B}}\right)$
49 48 23 eqeltrd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),{ℝ}^{*},<\right)\in ℝ$
50 supxrre3 ${⊢}\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\subseteq ℝ\wedge \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\ne \varnothing \right)\to \left(sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),{ℝ}^{*},<\right)\in ℝ↔\exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{t}\le {w}\right)$
51 44 46 50 syl2anc ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),{ℝ}^{*},<\right)\in ℝ↔\exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{t}\le {w}\right)$
52 49 51 mpbid ${⊢}{\phi }\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{t}\le {w}$
53 eqid ${⊢}\left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}=\left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}$
54 32 34 40 44 46 52 53 supadd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),ℝ,<\right)+sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),ℝ,<\right)=sup\left(\left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\},ℝ,<\right)$
55 simpl ${⊢}\left({\phi }\wedge {r}\in \left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}\right)\to {\phi }$
56 vex ${⊢}{r}\in \mathrm{V}$
57 eqeq1 ${⊢}{z}={r}\to \left({z}={v}+{u}↔{r}={v}+{u}\right)$
58 57 rexbidv ${⊢}{z}={r}\to \left(\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}↔\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}\right)$
59 58 rexbidv ${⊢}{z}={r}\to \left(\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}↔\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}\right)$
60 56 59 elab ${⊢}{r}\in \left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}↔\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}$
61 60 biimpi ${⊢}{r}\in \left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}\to \exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}$
62 61 adantl ${⊢}\left({\phi }\wedge {r}\in \left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}\right)\to \exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}$
63 simpl ${⊢}\left({\phi }\wedge \left({v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\wedge {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\right)\to {\phi }$
64 vex ${⊢}{v}\in \mathrm{V}$
65 sumeq1 ${⊢}{x}={a}\to \sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)$
66 65 cbvmptv ${⊢}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)=\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)$
67 66 elrnmpt ${⊢}{v}\in \mathrm{V}\to \left({v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)↔\exists {a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)$
68 64 67 ax-mp ${⊢}{v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)↔\exists {a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)$
69 68 biimpi ${⊢}{v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\to \exists {a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)$
70 69 adantr ${⊢}\left({v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\wedge {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\to \exists {a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)$
71 vex ${⊢}{u}\in \mathrm{V}$
72 sumeq1 ${⊢}{x}={b}\to \sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)$
73 72 cbvmptv ${⊢}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)=\left({b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)$
74 73 elrnmpt ${⊢}{u}\in \mathrm{V}\to \left({u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)↔\exists {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)$
75 71 74 ax-mp ${⊢}{u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)↔\exists {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)$
76 75 biimpi ${⊢}{u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\to \exists {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)$
77 76 adantl ${⊢}\left({v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\wedge {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\to \exists {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)$
78 70 77 jca ${⊢}\left({v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\wedge {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\to \left(\exists {a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge \exists {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)$
79 reeanv ${⊢}\exists {a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)↔\left(\exists {a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge \exists {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)$
80 78 79 sylibr ${⊢}\left({v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\wedge {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\to \exists {a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)$
81 80 adantl ${⊢}\left({\phi }\wedge \left({v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\wedge {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\right)\to \exists {a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)$
82 eqid ${⊢}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)=\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)$
83 elinel1 ${⊢}{a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to {a}\in 𝒫{A}$
84 elpwi ${⊢}{a}\in 𝒫{A}\to {a}\subseteq {A}$
85 id ${⊢}{a}\subseteq {A}\to {a}\subseteq {A}$
86 85 9 sstrdi ${⊢}{a}\subseteq {A}\to {a}\subseteq {U}$
87 84 86 syl ${⊢}{a}\in 𝒫{A}\to {a}\subseteq {U}$
88 83 87 syl ${⊢}{a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to {a}\subseteq {U}$
89 88 adantr ${⊢}\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\to {a}\subseteq {U}$
90 elinel1 ${⊢}{b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\to {b}\in 𝒫{B}$
91 elpwi ${⊢}{b}\in 𝒫{B}\to {b}\subseteq {B}$
92 id ${⊢}{b}\subseteq {B}\to {b}\subseteq {B}$
93 92 20 sstrdi ${⊢}{b}\subseteq {B}\to {b}\subseteq {U}$
94 91 93 syl ${⊢}{b}\in 𝒫{B}\to {b}\subseteq {U}$
95 90 94 syl ${⊢}{b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\to {b}\subseteq {U}$
96 95 adantl ${⊢}\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\to {b}\subseteq {U}$
97 89 96 unssd ${⊢}\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\to {a}\cup {b}\subseteq {U}$
98 vex ${⊢}{a}\in \mathrm{V}$
99 vex ${⊢}{b}\in \mathrm{V}$
100 98 99 unex ${⊢}{a}\cup {b}\in \mathrm{V}$
101 100 elpw ${⊢}{a}\cup {b}\in 𝒫{U}↔{a}\cup {b}\subseteq {U}$
102 97 101 sylibr ${⊢}\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\to {a}\cup {b}\in 𝒫{U}$
103 elinel2 ${⊢}{a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to {a}\in \mathrm{Fin}$
104 103 adantr ${⊢}\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\to {a}\in \mathrm{Fin}$
105 elinel2 ${⊢}{b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\to {b}\in \mathrm{Fin}$
106 105 adantl ${⊢}\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\to {b}\in \mathrm{Fin}$
107 unfi ${⊢}\left({a}\in \mathrm{Fin}\wedge {b}\in \mathrm{Fin}\right)\to {a}\cup {b}\in \mathrm{Fin}$
108 104 106 107 syl2anc ${⊢}\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\to {a}\cup {b}\in \mathrm{Fin}$
109 102 108 elind ${⊢}\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\to {a}\cup {b}\in \left(𝒫{U}\cap \mathrm{Fin}\right)$
110 109 adantl ${⊢}\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\to {a}\cup {b}\in \left(𝒫{U}\cap \mathrm{Fin}\right)$
111 110 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\wedge \left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\wedge {r}={v}+{u}\right)\to {a}\cup {b}\in \left(𝒫{U}\cap \mathrm{Fin}\right)$
112 simpl ${⊢}\left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\to {v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)$
113 simpr ${⊢}\left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\to {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)$
114 112 113 oveq12d ${⊢}\left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\to {v}+{u}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)+\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)$
115 114 adantl ${⊢}\left(\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\wedge \left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\to {v}+{u}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)+\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)$
116 83 84 syl ${⊢}{a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to {a}\subseteq {A}$
117 116 sselda ${⊢}\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {y}\in {a}\right)\to {y}\in {A}$
118 fvres ${⊢}{y}\in {A}\to \left({{F}↾}_{{A}}\right)\left({y}\right)={F}\left({y}\right)$
119 117 118 syl ${⊢}\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {y}\in {a}\right)\to \left({{F}↾}_{{A}}\right)\left({y}\right)={F}\left({y}\right)$
120 119 sumeq2dv ${⊢}{a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to \sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)=\sum _{{y}\in {a}}{F}\left({y}\right)$
121 120 adantr ${⊢}\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\to \sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)=\sum _{{y}\in {a}}{F}\left({y}\right)$
122 90 91 syl ${⊢}{b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\to {b}\subseteq {B}$
123 122 sselda ${⊢}\left({b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\wedge {y}\in {b}\right)\to {y}\in {B}$
124 fvres ${⊢}{y}\in {B}\to \left({{F}↾}_{{B}}\right)\left({y}\right)={F}\left({y}\right)$
125 123 124 syl ${⊢}\left({b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\wedge {y}\in {b}\right)\to \left({{F}↾}_{{B}}\right)\left({y}\right)={F}\left({y}\right)$
126 125 sumeq2dv ${⊢}{b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\to \sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)=\sum _{{y}\in {b}}{F}\left({y}\right)$
127 126 adantl ${⊢}\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\to \sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)=\sum _{{y}\in {b}}{F}\left({y}\right)$
128 121 127 oveq12d ${⊢}\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\to \sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)+\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)=\sum _{{y}\in {a}}{F}\left({y}\right)+\sum _{{y}\in {b}}{F}\left({y}\right)$
129 128 adantr ${⊢}\left(\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\wedge \left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\to \sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)+\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)=\sum _{{y}\in {a}}{F}\left({y}\right)+\sum _{{y}\in {b}}{F}\left({y}\right)$
130 115 129 eqtrd ${⊢}\left(\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\wedge \left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\to {v}+{u}=\sum _{{y}\in {a}}{F}\left({y}\right)+\sum _{{y}\in {b}}{F}\left({y}\right)$
131 130 ad4ant23 ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\wedge \left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\wedge {r}={v}+{u}\right)\to {v}+{u}=\sum _{{y}\in {a}}{F}\left({y}\right)+\sum _{{y}\in {b}}{F}\left({y}\right)$
132 simpr ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\wedge \left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\wedge {r}={v}+{u}\right)\to {r}={v}+{u}$
133 4 adantr ${⊢}\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\to {A}\cap {B}=\varnothing$
134 116 ad2antrl ${⊢}\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\to {a}\subseteq {A}$
135 122 adantl ${⊢}\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\to {b}\subseteq {B}$
136 135 adantl ${⊢}\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\to {b}\subseteq {B}$
137 ssin0 ${⊢}\left({A}\cap {B}=\varnothing \wedge {a}\subseteq {A}\wedge {b}\subseteq {B}\right)\to {a}\cap {b}=\varnothing$
138 133 134 136 137 syl3anc ${⊢}\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\to {a}\cap {b}=\varnothing$
139 eqidd ${⊢}\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\to {a}\cup {b}={a}\cup {b}$
140 108 adantl ${⊢}\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\to {a}\cup {b}\in \mathrm{Fin}$
141 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
142 ax-resscn ${⊢}ℝ\subseteq ℂ$
143 141 142 sstri ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℂ$
144 5 28 fge0iccico ${⊢}{\phi }\to {F}:{U}⟶\left[0,\mathrm{+\infty }\right)$
145 144 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\wedge {y}\in \left({a}\cup {b}\right)\right)\to {F}:{U}⟶\left[0,\mathrm{+\infty }\right)$
146 97 sselda ${⊢}\left(\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\wedge {y}\in \left({a}\cup {b}\right)\right)\to {y}\in {U}$
147 146 adantll ${⊢}\left(\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\wedge {y}\in \left({a}\cup {b}\right)\right)\to {y}\in {U}$
148 145 147 ffvelrnd ${⊢}\left(\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\wedge {y}\in \left({a}\cup {b}\right)\right)\to {F}\left({y}\right)\in \left[0,\mathrm{+\infty }\right)$
149 143 148 sseldi ${⊢}\left(\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\wedge {y}\in \left({a}\cup {b}\right)\right)\to {F}\left({y}\right)\in ℂ$
150 138 139 140 149 fsumsplit ${⊢}\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\to \sum _{{y}\in {a}\cup {b}}{F}\left({y}\right)=\sum _{{y}\in {a}}{F}\left({y}\right)+\sum _{{y}\in {b}}{F}\left({y}\right)$
151 150 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\wedge \left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\wedge {r}={v}+{u}\right)\to \sum _{{y}\in {a}\cup {b}}{F}\left({y}\right)=\sum _{{y}\in {a}}{F}\left({y}\right)+\sum _{{y}\in {b}}{F}\left({y}\right)$
152 131 132 151 3eqtr4d ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\wedge \left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\wedge {r}={v}+{u}\right)\to {r}=\sum _{{y}\in {a}\cup {b}}{F}\left({y}\right)$
153 sumeq1 ${⊢}{x}={a}\cup {b}\to \sum _{{y}\in {x}}{F}\left({y}\right)=\sum _{{y}\in {a}\cup {b}}{F}\left({y}\right)$
154 153 rspceeqv ${⊢}\left({a}\cup {b}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {r}=\sum _{{y}\in {a}\cup {b}}{F}\left({y}\right)\right)\to \exists {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{r}=\sum _{{y}\in {x}}{F}\left({y}\right)$
155 111 152 154 syl2anc ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\wedge \left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\wedge {r}={v}+{u}\right)\to \exists {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{r}=\sum _{{y}\in {x}}{F}\left({y}\right)$
156 56 a1i ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\wedge \left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\wedge {r}={v}+{u}\right)\to {r}\in \mathrm{V}$
157 82 155 156 elrnmptd ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\wedge \left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\wedge {r}={v}+{u}\right)\to {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)$
158 157 ex ${⊢}\left(\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\wedge \left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\to \left({r}={v}+{u}\to {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)$
159 158 ex ${⊢}\left({\phi }\wedge \left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\right)\to \left(\left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\to \left({r}={v}+{u}\to {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)\right)$
160 159 ex ${⊢}{\phi }\to \left(\left({a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\right)\to \left(\left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\to \left({r}={v}+{u}\to {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)\right)\right)$
161 160 rexlimdvv ${⊢}{\phi }\to \left(\exists {a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\to \left({r}={v}+{u}\to {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)\right)$
162 161 imp ${⊢}\left({\phi }\wedge \exists {a}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({v}=\sum _{{y}\in {a}}\left({{F}↾}_{{A}}\right)\left({y}\right)\wedge {u}=\sum _{{y}\in {b}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\to \left({r}={v}+{u}\to {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)$
163 63 81 162 syl2anc ${⊢}\left({\phi }\wedge \left({v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\wedge {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\right)\to \left({r}={v}+{u}\to {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)$
164 163 ex ${⊢}{\phi }\to \left(\left({v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\wedge {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\right)\to \left({r}={v}+{u}\to {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)\right)$
165 164 rexlimdvv ${⊢}{\phi }\to \left(\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}\to {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)$
166 165 imp ${⊢}\left({\phi }\wedge \exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}\right)\to {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)$
167 55 62 166 syl2anc ${⊢}\left({\phi }\wedge {r}\in \left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}\right)\to {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)$
168 167 ex ${⊢}{\phi }\to \left({r}\in \left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}\to {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)$
169 82 elrnmpt ${⊢}{r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to \left({r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)↔\exists {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{r}=\sum _{{y}\in {x}}{F}\left({y}\right)\right)$
170 169 ibi ${⊢}{r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to \exists {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{r}=\sum _{{y}\in {x}}{F}\left({y}\right)$
171 170 adantl ${⊢}\left({\phi }\wedge {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)\to \exists {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{r}=\sum _{{y}\in {x}}{F}\left({y}\right)$
172 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
173 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{r}$
174 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)$
175 174 nfrn ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)$
176 173 175 nfel ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)$
177 172 176 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)$
178 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)$
179 178 nfrn ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)$
180 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)$
181 180 nfrn ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)$
182 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{r}={v}+{u}$
183 181 182 nfrex ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}$
184 179 183 nfrex ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}$
185 inss2 ${⊢}{x}\cap {A}\subseteq {A}$
186 185 sseli ${⊢}{y}\in \left({x}\cap {A}\right)\to {y}\in {A}$
187 186 adantl ${⊢}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {y}\in \left({x}\cap {A}\right)\right)\to {y}\in {A}$
188 118 eqcomd ${⊢}{y}\in {A}\to {F}\left({y}\right)=\left({{F}↾}_{{A}}\right)\left({y}\right)$
189 187 188 syl ${⊢}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {y}\in \left({x}\cap {A}\right)\right)\to {F}\left({y}\right)=\left({{F}↾}_{{A}}\right)\left({y}\right)$
190 189 sumeq2dv ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to \sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)=\sum _{{y}\in {x}\cap {A}}\left({{F}↾}_{{A}}\right)\left({y}\right)$
191 sumeq1 ${⊢}{x}={z}\to \sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)=\sum _{{y}\in {z}}\left({{F}↾}_{{A}}\right)\left({y}\right)$
192 191 cbvmptv ${⊢}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)=\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {z}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)$
193 vex ${⊢}{x}\in \mathrm{V}$
194 193 inex1 ${⊢}{x}\cap {A}\in \mathrm{V}$
195 194 elpw ${⊢}{x}\cap {A}\in 𝒫{A}↔{x}\cap {A}\subseteq {A}$
196 185 195 mpbir ${⊢}{x}\cap {A}\in 𝒫{A}$
197 196 a1i ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to {x}\cap {A}\in 𝒫{A}$
198 elinel2 ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to {x}\in \mathrm{Fin}$
199 inss1 ${⊢}{x}\cap {A}\subseteq {x}$
200 199 a1i ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to {x}\cap {A}\subseteq {x}$
201 ssfi ${⊢}\left({x}\in \mathrm{Fin}\wedge {x}\cap {A}\subseteq {x}\right)\to {x}\cap {A}\in \mathrm{Fin}$
202 198 200 201 syl2anc ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to {x}\cap {A}\in \mathrm{Fin}$
203 197 202 elind ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to {x}\cap {A}\in \left(𝒫{A}\cap \mathrm{Fin}\right)$
204 eqidd ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to \sum _{{y}\in {x}\cap {A}}\left({{F}↾}_{{A}}\right)\left({y}\right)=\sum _{{y}\in {x}\cap {A}}\left({{F}↾}_{{A}}\right)\left({y}\right)$
205 sumeq1 ${⊢}{z}={x}\cap {A}\to \sum _{{y}\in {z}}\left({{F}↾}_{{A}}\right)\left({y}\right)=\sum _{{y}\in {x}\cap {A}}\left({{F}↾}_{{A}}\right)\left({y}\right)$
206 205 rspceeqv ${⊢}\left({x}\cap {A}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \sum _{{y}\in {x}\cap {A}}\left({{F}↾}_{{A}}\right)\left({y}\right)=\sum _{{y}\in {x}\cap {A}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\to \exists {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\sum _{{y}\in {x}\cap {A}}\left({{F}↾}_{{A}}\right)\left({y}\right)=\sum _{{y}\in {z}}\left({{F}↾}_{{A}}\right)\left({y}\right)$
207 203 204 206 syl2anc ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to \exists {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\sum _{{y}\in {x}\cap {A}}\left({{F}↾}_{{A}}\right)\left({y}\right)=\sum _{{y}\in {z}}\left({{F}↾}_{{A}}\right)\left({y}\right)$
208 sumex ${⊢}\sum _{{y}\in {x}\cap {A}}\left({{F}↾}_{{A}}\right)\left({y}\right)\in \mathrm{V}$
209 208 a1i ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to \sum _{{y}\in {x}\cap {A}}\left({{F}↾}_{{A}}\right)\left({y}\right)\in \mathrm{V}$
210 192 207 209 elrnmptd ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to \sum _{{y}\in {x}\cap {A}}\left({{F}↾}_{{A}}\right)\left({y}\right)\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)$
211 190 210 eqeltrd ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to \sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)$
212 211 3ad2ant2 ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {r}=\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to \sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)$
213 sumeq1 ${⊢}{x}={z}\to \sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)=\sum _{{y}\in {z}}\left({{F}↾}_{{B}}\right)\left({y}\right)$
214 213 cbvmptv ${⊢}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)=\left({z}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {z}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)$
215 inss2 ${⊢}{x}\cap {B}\subseteq {B}$
216 193 inex1 ${⊢}{x}\cap {B}\in \mathrm{V}$
217 216 elpw ${⊢}{x}\cap {B}\in 𝒫{B}↔{x}\cap {B}\subseteq {B}$
218 215 217 mpbir ${⊢}{x}\cap {B}\in 𝒫{B}$
219 218 a1i ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {r}=\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to {x}\cap {B}\in 𝒫{B}$
220 inss1 ${⊢}{x}\cap {B}\subseteq {x}$
221 220 a1i ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to {x}\cap {B}\subseteq {x}$
222 ssfi ${⊢}\left({x}\in \mathrm{Fin}\wedge {x}\cap {B}\subseteq {x}\right)\to {x}\cap {B}\in \mathrm{Fin}$
223 198 221 222 syl2anc ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to {x}\cap {B}\in \mathrm{Fin}$
224 223 3ad2ant2 ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {r}=\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to {x}\cap {B}\in \mathrm{Fin}$
225 219 224 elind ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {r}=\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to {x}\cap {B}\in \left(𝒫{B}\cap \mathrm{Fin}\right)$
226 215 sseli ${⊢}{y}\in \left({x}\cap {B}\right)\to {y}\in {B}$
227 124 eqcomd ${⊢}{y}\in {B}\to {F}\left({y}\right)=\left({{F}↾}_{{B}}\right)\left({y}\right)$
228 226 227 syl ${⊢}{y}\in \left({x}\cap {B}\right)\to {F}\left({y}\right)=\left({{F}↾}_{{B}}\right)\left({y}\right)$
229 228 sumeq2i ${⊢}\sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)=\sum _{{y}\in {x}\cap {B}}\left({{F}↾}_{{B}}\right)\left({y}\right)$
230 229 a1i ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\right)\to \sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)=\sum _{{y}\in {x}\cap {B}}\left({{F}↾}_{{B}}\right)\left({y}\right)$
231 230 3adant3 ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {r}=\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to \sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)=\sum _{{y}\in {x}\cap {B}}\left({{F}↾}_{{B}}\right)\left({y}\right)$
232 sumeq1 ${⊢}{z}={x}\cap {B}\to \sum _{{y}\in {z}}\left({{F}↾}_{{B}}\right)\left({y}\right)=\sum _{{y}\in {x}\cap {B}}\left({{F}↾}_{{B}}\right)\left({y}\right)$
233 232 rspceeqv ${⊢}\left({x}\cap {B}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\wedge \sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)=\sum _{{y}\in {x}\cap {B}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\to \exists {z}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)=\sum _{{y}\in {z}}\left({{F}↾}_{{B}}\right)\left({y}\right)$
234 225 231 233 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {r}=\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to \exists {z}\in \left(𝒫{B}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)=\sum _{{y}\in {z}}\left({{F}↾}_{{B}}\right)\left({y}\right)$
235 sumex ${⊢}\sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)\in \mathrm{V}$
236 235 a1i ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {r}=\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to \sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)\in \mathrm{V}$
237 214 234 236 elrnmptd ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {r}=\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to \sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)$
238 simp3 ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {r}=\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to {r}=\sum _{{y}\in {x}}{F}\left({y}\right)$
239 185 a1i ${⊢}{\phi }\to {x}\cap {A}\subseteq {A}$
240 215 a1i ${⊢}{\phi }\to {x}\cap {B}\subseteq {B}$
241 ssin0 ${⊢}\left({A}\cap {B}=\varnothing \wedge {x}\cap {A}\subseteq {A}\wedge {x}\cap {B}\subseteq {B}\right)\to \left({x}\cap {A}\right)\cap \left({x}\cap {B}\right)=\varnothing$
242 4 239 240 241 syl3anc ${⊢}{\phi }\to \left({x}\cap {A}\right)\cap \left({x}\cap {B}\right)=\varnothing$
243 242 adantr ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\right)\to \left({x}\cap {A}\right)\cap \left({x}\cap {B}\right)=\varnothing$
244 elinel1 ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to {x}\in 𝒫{U}$
245 elpwi ${⊢}{x}\in 𝒫{U}\to {x}\subseteq {U}$
246 244 245 syl ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to {x}\subseteq {U}$
247 3 ineq2i ${⊢}{x}\cap {U}={x}\cap \left({A}\cup {B}\right)$
248 247 a1i ${⊢}{x}\subseteq {U}\to {x}\cap {U}={x}\cap \left({A}\cup {B}\right)$
249 dfss ${⊢}{x}\subseteq {U}↔{x}={x}\cap {U}$
250 249 biimpi ${⊢}{x}\subseteq {U}\to {x}={x}\cap {U}$
251 indi ${⊢}{x}\cap \left({A}\cup {B}\right)=\left({x}\cap {A}\right)\cup \left({x}\cap {B}\right)$
252 251 eqcomi ${⊢}\left({x}\cap {A}\right)\cup \left({x}\cap {B}\right)={x}\cap \left({A}\cup {B}\right)$
253 252 a1i ${⊢}{x}\subseteq {U}\to \left({x}\cap {A}\right)\cup \left({x}\cap {B}\right)={x}\cap \left({A}\cup {B}\right)$
254 248 250 253 3eqtr4d ${⊢}{x}\subseteq {U}\to {x}=\left({x}\cap {A}\right)\cup \left({x}\cap {B}\right)$
255 246 254 syl ${⊢}{x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to {x}=\left({x}\cap {A}\right)\cup \left({x}\cap {B}\right)$
256 255 adantl ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\right)\to {x}=\left({x}\cap {A}\right)\cup \left({x}\cap {B}\right)$
257 198 adantl ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\right)\to {x}\in \mathrm{Fin}$
258 144 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\right)\wedge {y}\in {x}\right)\to {F}:{U}⟶\left[0,\mathrm{+\infty }\right)$
259 246 sselda ${⊢}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {y}\in {x}\right)\to {y}\in {U}$
260 259 adantll ${⊢}\left(\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\right)\wedge {y}\in {x}\right)\to {y}\in {U}$
261 258 260 ffvelrnd ${⊢}\left(\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\right)\wedge {y}\in {x}\right)\to {F}\left({y}\right)\in \left[0,\mathrm{+\infty }\right)$
262 143 261 sseldi ${⊢}\left(\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\right)\wedge {y}\in {x}\right)\to {F}\left({y}\right)\in ℂ$
263 243 256 257 262 fsumsplit ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\right)\to \sum _{{y}\in {x}}{F}\left({y}\right)=\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)+\sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)$
264 263 3adant3 ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {r}=\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to \sum _{{y}\in {x}}{F}\left({y}\right)=\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)+\sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)$
265 238 264 eqtrd ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {r}=\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to {r}=\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)+\sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)$
266 oveq2 ${⊢}{u}=\sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)\to \sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)+{u}=\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)+\sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)$
267 266 rspceeqv ${⊢}\left(\sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\wedge {r}=\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)+\sum _{{y}\in {x}\cap {B}}{F}\left({y}\right)\right)\to \exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}=\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)+{u}$
268 237 265 267 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {r}=\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to \exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}=\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)+{u}$
269 oveq1 ${⊢}{v}=\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)\to {v}+{u}=\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)+{u}$
270 269 eqeq2d ${⊢}{v}=\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)\to \left({r}={v}+{u}↔{r}=\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)+{u}\right)$
271 270 rexbidv ${⊢}{v}=\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)\to \left(\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}↔\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}=\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)+{u}\right)$
272 271 rspcev ${⊢}\left(\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\wedge \exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}=\sum _{{y}\in {x}\cap {A}}{F}\left({y}\right)+{u}\right)\to \exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}$
273 212 268 272 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\wedge {r}=\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to \exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}$
274 273 3exp ${⊢}{\phi }\to \left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to \left({r}=\sum _{{y}\in {x}}{F}\left({y}\right)\to \exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}\right)\right)$
275 274 adantr ${⊢}\left({\phi }\wedge {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)\to \left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\to \left({r}=\sum _{{y}\in {x}}{F}\left({y}\right)\to \exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}\right)\right)$
276 177 184 275 rexlimd ${⊢}\left({\phi }\wedge {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)\to \left(\exists {x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{r}=\sum _{{y}\in {x}}{F}\left({y}\right)\to \exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}\right)$
277 171 276 mpd ${⊢}\left({\phi }\wedge {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)\to \exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{r}={v}+{u}$
278 277 60 sylibr ${⊢}\left({\phi }\wedge {r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)\to {r}\in \left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}$
279 278 ex ${⊢}{\phi }\to \left({r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\to {r}\in \left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}\right)$
280 168 279 impbid ${⊢}{\phi }\to \left({r}\in \left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}↔{r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)$
281 280 alrimiv ${⊢}{\phi }\to \forall {r}\phantom{\rule{.4em}{0ex}}\left({r}\in \left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}↔{r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)$
282 dfcleq ${⊢}\left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}=\mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)↔\forall {r}\phantom{\rule{.4em}{0ex}}\left({r}\in \left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}↔{r}\in \mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)\right)$
283 281 282 sylibr ${⊢}{\phi }\to \left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\}=\mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right)$
284 283 supeq1d ${⊢}{\phi }\to sup\left(\left\{{z}|\exists {v}\in \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={v}+{u}\right\},ℝ,<\right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right),ℝ,<\right)$
285 27 54 284 3eqtrrd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right),ℝ,<\right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),ℝ,<\right){+}_{𝑒}sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),ℝ,<\right)$
286 15 5 6 sge0supre ${⊢}{\phi }\to \mathrm{sum^}\left({F}\right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫{U}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}{F}\left({y}\right)\right),ℝ,<\right)$
287 17 24 oveq12d ${⊢}{\phi }\to \mathrm{sum^}\left({{F}↾}_{{A}}\right){+}_{𝑒}\mathrm{sum^}\left({{F}↾}_{{B}}\right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{A}}\right)\left({y}\right)\right),ℝ,<\right){+}_{𝑒}sup\left(\mathrm{ran}\left({x}\in \left(𝒫{B}\cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\left({{F}↾}_{{B}}\right)\left({y}\right)\right),ℝ,<\right)$
288 285 286 287 3eqtr4d ${⊢}{\phi }\to \mathrm{sum^}\left({F}\right)=\mathrm{sum^}\left({{F}↾}_{{A}}\right){+}_{𝑒}\mathrm{sum^}\left({{F}↾}_{{B}}\right)$
289 rexadd ${⊢}\left(\mathrm{sum^}\left({{F}↾}_{{A}}\right)\in ℝ\wedge \mathrm{sum^}\left({{F}↾}_{{B}}\right)\in ℝ\right)\to \mathrm{sum^}\left({{F}↾}_{{A}}\right){+}_{𝑒}\mathrm{sum^}\left({{F}↾}_{{B}}\right)=\mathrm{sum^}\left({{F}↾}_{{A}}\right)+\mathrm{sum^}\left({{F}↾}_{{B}}\right)$
290 16 23 289 syl2anc ${⊢}{\phi }\to \mathrm{sum^}\left({{F}↾}_{{A}}\right){+}_{𝑒}\mathrm{sum^}\left({{F}↾}_{{B}}\right)=\mathrm{sum^}\left({{F}↾}_{{A}}\right)+\mathrm{sum^}\left({{F}↾}_{{B}}\right)$
291 288 290 eqtrd ${⊢}{\phi }\to \mathrm{sum^}\left({F}\right)=\mathrm{sum^}\left({{F}↾}_{{A}}\right)+\mathrm{sum^}\left({{F}↾}_{{B}}\right)$