Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sge0iunmptlemre Structured version   Visualization version   GIF version

Theorem sge0iunmptlemre 45775
Description: Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
sge0iunmptlemre.a (𝜑𝐴𝑉)
sge0iunmptlemre.b ((𝜑𝑥𝐴) → 𝐵𝑊)
sge0iunmptlemre.dj (𝜑Disj 𝑥𝐴 𝐵)
sge0iunmptlemre.c ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
sge0iunmptlemre.re ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
sge0iunmptlemre.sxr (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ∈ ℝ*)
sge0iunmptlemre.ssxr (𝜑 → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ∈ ℝ*)
sge0iunmptlemre.f (𝜑 → (𝑘 𝑥𝐴 𝐵𝐶): 𝑥𝐴 𝐵⟶(0[,]+∞))
sge0iunmptlemre.iue (𝜑 𝑥𝐴 𝐵 ∈ V)
Assertion
Ref Expression
sge0iunmptlemre (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
Distinct variable groups:   𝐴,𝑘,𝑥   𝐵,𝑘   𝑥,𝐶   𝑥,𝑊   𝜑,𝑘,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑘)   𝑉(𝑥,𝑘)   𝑊(𝑘)

Proof of Theorem sge0iunmptlemre
Dummy variables 𝑏 𝑝 𝑦 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sge0iunmptlemre.sxr . 2 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ∈ ℝ*)
2 sge0iunmptlemre.ssxr . 2 (𝜑 → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ∈ ℝ*)
3 elpwinss 44385 . . . . . . . . . 10 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → 𝑦 𝑥𝐴 𝐵)
43resmptd 6038 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → ((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦) = (𝑘𝑦𝐶))
54fveq2d 6895 . . . . . . . 8 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = (Σ^‘(𝑘𝑦𝐶)))
65adantl 481 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = (Σ^‘(𝑘𝑦𝐶)))
7 elinel2 4192 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
87adantl 481 . . . . . . . 8 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → 𝑦 ∈ Fin)
93sselda 3978 . . . . . . . . . . 11 ((𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) ∧ 𝑘𝑦) → 𝑘 𝑥𝐴 𝐵)
10 eliun 4995 . . . . . . . . . . 11 (𝑘 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑘𝐵)
119, 10sylib 217 . . . . . . . . . 10 ((𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) ∧ 𝑘𝑦) → ∃𝑥𝐴 𝑘𝐵)
1211adantll 713 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → ∃𝑥𝐴 𝑘𝐵)
13 nfv 1910 . . . . . . . . . . . 12 𝑥𝜑
14 nfcv 2898 . . . . . . . . . . . . 13 𝑥𝑦
15 nfiu1 5025 . . . . . . . . . . . . . . 15 𝑥 𝑥𝐴 𝐵
1615nfpw 4617 . . . . . . . . . . . . . 14 𝑥𝒫 𝑥𝐴 𝐵
17 nfcv 2898 . . . . . . . . . . . . . 14 𝑥Fin
1816, 17nfin 4212 . . . . . . . . . . . . 13 𝑥(𝒫 𝑥𝐴 𝐵 ∩ Fin)
1914, 18nfel 2912 . . . . . . . . . . . 12 𝑥 𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)
2013, 19nfan 1895 . . . . . . . . . . 11 𝑥(𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
21 nfv 1910 . . . . . . . . . . 11 𝑥 𝑘𝑦
2220, 21nfan 1895 . . . . . . . . . 10 𝑥((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦)
23 nfv 1910 . . . . . . . . . 10 𝑥 𝐶 ∈ (0[,)+∞)
24 simp3 1136 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → 𝑘𝐵)
25 sge0iunmptlemre.c . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
26 eqid 2727 . . . . . . . . . . . . . . . 16 (𝑘𝐵𝐶) = (𝑘𝐵𝐶)
2726fvmpt2 7010 . . . . . . . . . . . . . . 15 ((𝑘𝐵𝐶 ∈ (0[,]+∞)) → ((𝑘𝐵𝐶)‘𝑘) = 𝐶)
2824, 25, 27syl2anc 583 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → ((𝑘𝐵𝐶)‘𝑘) = 𝐶)
2928eqcomd 2733 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 = ((𝑘𝐵𝐶)‘𝑘))
30253expa 1116 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
3130, 26fmptd 7118 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
32313adant3 1130 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
33 sge0iunmptlemre.b . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → 𝐵𝑊)
34333adant3 1130 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴𝑘𝐵) → 𝐵𝑊)
35 sge0iunmptlemre.re . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
36353adant3 1130 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴𝑘𝐵) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
3734, 32, 36sge0rern 45748 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → ¬ +∞ ∈ ran (𝑘𝐵𝐶))
3832, 37fge0iccico 45730 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → (𝑘𝐵𝐶):𝐵⟶(0[,)+∞))
3938, 24ffvelcdmd 7089 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴𝑘𝐵) → ((𝑘𝐵𝐶)‘𝑘) ∈ (0[,)+∞))
4029, 39eqeltrd 2828 . . . . . . . . . . . 12 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,)+∞))
41403exp 1117 . . . . . . . . . . 11 (𝜑 → (𝑥𝐴 → (𝑘𝐵𝐶 ∈ (0[,)+∞))))
4241ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → (𝑥𝐴 → (𝑘𝐵𝐶 ∈ (0[,)+∞))))
4322, 23, 42rexlimd 3258 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → (∃𝑥𝐴 𝑘𝐵𝐶 ∈ (0[,)+∞)))
4412, 43mpd 15 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → 𝐶 ∈ (0[,)+∞))
458, 44sge0fsummpt 45750 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑦𝐶)) = Σ𝑘𝑦 𝐶)
46 sseqin2 4211 . . . . . . . . . . . . . 14 (𝑦 𝑥𝐴 𝐵 ↔ ( 𝑥𝐴 𝐵𝑦) = 𝑦)
4746biimpi 215 . . . . . . . . . . . . 13 (𝑦 𝑥𝐴 𝐵 → ( 𝑥𝐴 𝐵𝑦) = 𝑦)
4847eqcomd 2733 . . . . . . . . . . . 12 (𝑦 𝑥𝐴 𝐵𝑦 = ( 𝑥𝐴 𝐵𝑦))
49 iunin1 5069 . . . . . . . . . . . . 13 𝑥𝐴 (𝐵𝑦) = ( 𝑥𝐴 𝐵𝑦)
5049a1i 11 . . . . . . . . . . . 12 (𝑦 𝑥𝐴 𝐵 𝑥𝐴 (𝐵𝑦) = ( 𝑥𝐴 𝐵𝑦))
5148, 50eqtr4d 2770 . . . . . . . . . . 11 (𝑦 𝑥𝐴 𝐵𝑦 = 𝑥𝐴 (𝐵𝑦))
523, 51syl 17 . . . . . . . . . 10 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → 𝑦 = 𝑥𝐴 (𝐵𝑦))
5352sumeq1d 15673 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → Σ𝑘𝑦 𝐶 = Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶)
5453adantl 481 . . . . . . . 8 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑘𝑦 𝐶 = Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶)
55 simpl 482 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → 𝜑)
5633adantlr 714 . . . . . . . . . 10 (((𝜑𝑦 ∈ Fin) ∧ 𝑥𝐴) → 𝐵𝑊)
57 sge0iunmptlemre.dj . . . . . . . . . . 11 (𝜑Disj 𝑥𝐴 𝐵)
5857adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → Disj 𝑥𝐴 𝐵)
59 rge0ssre 13459 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ ℝ
60 ax-resscn 11189 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
6159, 60sstri 3987 . . . . . . . . . . . 12 (0[,)+∞) ⊆ ℂ
6261, 40sselid 3976 . . . . . . . . . . 11 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ ℂ)
63623adant1r 1175 . . . . . . . . . 10 (((𝜑𝑦 ∈ Fin) ∧ 𝑥𝐴𝑘𝐵) → 𝐶 ∈ ℂ)
64 simpr 484 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → 𝑦 ∈ Fin)
6556, 58, 63, 64fsumiunss 44935 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶 = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
6655, 8, 65syl2anc 583 . . . . . . . 8 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶 = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
6754, 66eqtrd 2767 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑘𝑦 𝐶 = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
686, 45, 673eqtrd 2771 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
6956, 58, 64disjinfi 44537 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ∈ Fin)
70 id 22 . . . . . . . . . . . . 13 (𝑦 ∈ Fin → 𝑦 ∈ Fin)
71 inss2 4225 . . . . . . . . . . . . . 14 (𝑤 / 𝑥𝐵𝑦) ⊆ 𝑦
7271a1i 11 . . . . . . . . . . . . 13 (𝑦 ∈ Fin → (𝑤 / 𝑥𝐵𝑦) ⊆ 𝑦)
73 ssfi 9191 . . . . . . . . . . . . 13 ((𝑦 ∈ Fin ∧ (𝑤 / 𝑥𝐵𝑦) ⊆ 𝑦) → (𝑤 / 𝑥𝐵𝑦) ∈ Fin)
7470, 72, 73syl2anc 583 . . . . . . . . . . . 12 (𝑦 ∈ Fin → (𝑤 / 𝑥𝐵𝑦) ∈ Fin)
7574ad2antlr 726 . . . . . . . . . . 11 (((𝜑𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (𝑤 / 𝑥𝐵𝑦) ∈ Fin)
76 simpll 766 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝜑)
77 elrabi 3674 . . . . . . . . . . . . . 14 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} → 𝑤𝐴)
7877ad2antlr 726 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑤𝐴)
79 elinel1 4191 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) → 𝑘𝑤 / 𝑥𝐵)
8079adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑘𝑤 / 𝑥𝐵)
81 nfv 1910 . . . . . . . . . . . . . . . 16 𝑥 𝑤𝐴
82 nfcv 2898 . . . . . . . . . . . . . . . . 17 𝑥𝑘
83 nfcsb1v 3914 . . . . . . . . . . . . . . . . 17 𝑥𝑤 / 𝑥𝐵
8482, 83nfel 2912 . . . . . . . . . . . . . . . 16 𝑥 𝑘𝑤 / 𝑥𝐵
8513, 81, 84nf3an 1897 . . . . . . . . . . . . . . 15 𝑥(𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵)
8685, 23nfim 1892 . . . . . . . . . . . . . 14 𝑥((𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵) → 𝐶 ∈ (0[,)+∞))
87 eleq1w 2811 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
88 csbeq1a 3903 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
8988eleq2d 2814 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑘𝐵𝑘𝑤 / 𝑥𝐵))
9087, 893anbi23d 1436 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → ((𝜑𝑥𝐴𝑘𝐵) ↔ (𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵)))
9190imbi1d 341 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,)+∞)) ↔ ((𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵) → 𝐶 ∈ (0[,)+∞))))
9286, 91, 40chvarfv 2226 . . . . . . . . . . . . 13 ((𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵) → 𝐶 ∈ (0[,)+∞))
9376, 78, 80, 92syl3anc 1369 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
9493adantllr 718 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
9575, 94fsumge0cl 44933 . . . . . . . . . 10 (((𝜑𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶 ∈ (0[,)+∞))
9669, 95sge0fsummpt 45750 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)) = Σ𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
97 inss2 4225 . . . . . . . . . . . . . . . . 17 (𝐵𝑦) ⊆ 𝑦
9897a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ Fin → (𝐵𝑦) ⊆ 𝑦)
99 ssfi 9191 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ Fin ∧ (𝐵𝑦) ⊆ 𝑦) → (𝐵𝑦) ∈ Fin)
10070, 98, 99syl2anc 583 . . . . . . . . . . . . . . 15 (𝑦 ∈ Fin → (𝐵𝑦) ∈ Fin)
101100ad2antlr 726 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (𝐵𝑦) ∈ Fin)
102 simpll 766 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝜑)
103 rabid 3447 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↔ (𝑥𝐴 ∧ (𝐵𝑦) ≠ ∅))
104103biimpi 215 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} → (𝑥𝐴 ∧ (𝐵𝑦) ≠ ∅))
105104simpld 494 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} → 𝑥𝐴)
106105ad2antlr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝑥𝐴)
107 elinel1 4191 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (𝐵𝑦) → 𝑘𝐵)
108107adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝑘𝐵)
109102, 106, 108, 40syl3anc 1369 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
110109adantllr 718 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
111101, 110sge0fsummpt 45750 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) = Σ𝑘 ∈ (𝐵𝑦)𝐶)
112111mpteq2dva 5242 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ Fin) → (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))) = (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵𝑦)𝐶))
113 nfrab1 3446 . . . . . . . . . . . . . 14 𝑥{𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}
114 nfcv 2898 . . . . . . . . . . . . . 14 𝑤{𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}
115 nfcv 2898 . . . . . . . . . . . . . 14 𝑤Σ𝑘 ∈ (𝐵𝑦)𝐶
11683, 14nfin 4212 . . . . . . . . . . . . . . 15 𝑥(𝑤 / 𝑥𝐵𝑦)
117 nfcv 2898 . . . . . . . . . . . . . . 15 𝑥𝐶
118116, 117nfsum 15663 . . . . . . . . . . . . . 14 𝑥Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶
11988ineq1d 4207 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝐵𝑦) = (𝑤 / 𝑥𝐵𝑦))
120119sumeq1d 15673 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → Σ𝑘 ∈ (𝐵𝑦)𝐶 = Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
121113, 114, 115, 118, 120cbvmptf 5251 . . . . . . . . . . . . 13 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵𝑦)𝐶) = (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
122121a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ Fin) → (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵𝑦)𝐶) = (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶))
123112, 122eqtr2d 2768 . . . . . . . . . . 11 ((𝜑𝑦 ∈ Fin) → (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶) = (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))))
124123fveq2d 6895 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)) = (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
125124eqcomd 2733 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)))
126120, 114, 113, 115, 118cbvsum 15667 . . . . . . . . . 10 Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶 = Σ𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶
127126a1i 11 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶 = Σ𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
12896, 125, 1273eqtr4d 2777 . . . . . . . 8 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
12955, 8, 128syl2anc 583 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
130129eqcomd 2733 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶 = (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
13168, 130eqtrd 2767 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
132 sge0iunmptlemre.a . . . . . . . . 9 (𝜑𝐴𝑉)
13377ssriv 3982 . . . . . . . . . 10 {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ⊆ 𝐴
134133a1i 11 . . . . . . . . 9 (𝜑 → {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ⊆ 𝐴)
135132, 134ssexd 5318 . . . . . . . 8 (𝜑 → {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ∈ V)
136 vex 3473 . . . . . . . . . . . . 13 𝑦 ∈ V
137136inex2 5312 . . . . . . . . . . . 12 (𝑤 / 𝑥𝐵𝑦) ∈ V
138137a1i 11 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (𝑤 / 𝑥𝐵𝑦) ∈ V)
139 icossicc 13439 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ (0[,]+∞)
140 simpll 766 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝜑)
141 simplr 768 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑤𝐴)
14279adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑘𝑤 / 𝑥𝐵)
143140, 141, 142, 92syl3anc 1369 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
144139, 143sselid 3976 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,]+∞))
145 eqid 2727 . . . . . . . . . . . 12 (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶) = (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)
146144, 145fmptd 7118 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶):(𝑤 / 𝑥𝐵𝑦)⟶(0[,]+∞))
147138, 146sge0cl 45741 . . . . . . . . . 10 ((𝜑𝑤𝐴) → (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
14877, 147sylan2 592 . . . . . . . . 9 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
149 nfcv 2898 . . . . . . . . . 10 𝑤^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))
150 nfcv 2898 . . . . . . . . . . 11 𝑥Σ^
151116, 117nfmpt 5249 . . . . . . . . . . 11 𝑥(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)
152150, 151nffv 6901 . . . . . . . . . 10 𝑥^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))
153119mpteq1d 5237 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑘 ∈ (𝐵𝑦) ↦ 𝐶) = (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))
154153fveq2d 6895 . . . . . . . . . 10 (𝑥 = 𝑤 → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) = (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
155113, 114, 149, 152, 154cbvmptf 5251 . . . . . . . . 9 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))) = (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
156148, 155fmptd 7118 . . . . . . . 8 (𝜑 → (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))):{𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}⟶(0[,]+∞))
157135, 156sge0xrcl 45745 . . . . . . 7 (𝜑 → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
158157adantr 480 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
159 eqid 2727 . . . . . . . . 9 (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))) = (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
160147, 159fmptd 7118 . . . . . . . 8 (𝜑 → (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))):𝐴⟶(0[,]+∞))
161132, 160sge0xrcl 45745 . . . . . . 7 (𝜑 → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
162161adantr 480 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
16355, 2syl 17 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ∈ ℝ*)
164155fveq2i 6894 . . . . . . . . 9 ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))))
165164a1i 11 . . . . . . . 8 (𝜑 → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
166132, 147, 134sge0lessmpt 45759 . . . . . . . 8 (𝜑 → (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
167165, 166eqbrtrd 5164 . . . . . . 7 (𝜑 → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
168167adantr 480 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
169149, 152, 154cbvmpt 5253 . . . . . . . . . . 11 (𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))) = (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
170169eqcomi 2736 . . . . . . . . . 10 (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))
171170fveq2i 6894 . . . . . . . . 9 ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))))
172171a1i 11 . . . . . . . 8 (𝜑 → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
173136inex2 5312 . . . . . . . . . . 11 (𝐵𝑦) ∈ V
174173a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐵𝑦) ∈ V)
175107, 30sylan2 592 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝐶 ∈ (0[,]+∞))
176 eqid 2727 . . . . . . . . . . 11 (𝑘 ∈ (𝐵𝑦) ↦ 𝐶) = (𝑘 ∈ (𝐵𝑦) ↦ 𝐶)
177175, 176fmptd 7118 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑘 ∈ (𝐵𝑦) ↦ 𝐶):(𝐵𝑦)⟶(0[,]+∞))
178174, 177sge0cl 45741 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
17933, 31sge0cl 45741 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,]+∞))
180 inss1 4224 . . . . . . . . . . 11 (𝐵𝑦) ⊆ 𝐵
181180a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐵𝑦) ⊆ 𝐵)
18233, 30, 181sge0lessmpt 45759 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) ≤ (Σ^‘(𝑘𝐵𝐶)))
18313, 132, 178, 179, 182sge0lempt 45770 . . . . . . . 8 (𝜑 → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
184172, 183eqbrtrd 5164 . . . . . . 7 (𝜑 → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
185184adantr 480 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
186158, 162, 163, 168, 185xrletrd 13167 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
187131, 186eqbrtrd 5164 . . . 4 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
188187ralrimiva 3141 . . 3 (𝜑 → ∀𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)(Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
189 sge0iunmptlemre.iue . . . 4 (𝜑 𝑥𝐴 𝐵 ∈ V)
190 sge0iunmptlemre.f . . . 4 (𝜑 → (𝑘 𝑥𝐴 𝐵𝐶): 𝑥𝐴 𝐵⟶(0[,]+∞))
191189, 190, 2sge0lefi 45758 . . 3 (𝜑 → ((Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ ∀𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)(Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))))
192188, 191mpbird 257 . 2 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
193 elpwinss 44385 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦𝐴)
194193resmptd 6038 . . . . . . . 8 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → ((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦) = (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))))
195194fveq2d 6895 . . . . . . 7 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))))
196195adantl 481 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))))
197 elinel2 4192 . . . . . . . 8 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
198197adantl 481 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin)
199 0xr 11285 . . . . . . . . 9 0 ∈ ℝ*
200199a1i 11 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 0 ∈ ℝ*)
201 pnfxr 11292 . . . . . . . . 9 +∞ ∈ ℝ*
202201a1i 11 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → +∞ ∈ ℝ*)
203 simpll 766 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 𝜑)
204193sselda 3978 . . . . . . . . . . 11 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑥𝑦) → 𝑥𝐴)
205204adantll 713 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 𝑥𝐴)
206203, 205, 33syl2anc 583 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 𝐵𝑊)
207203, 205, 31syl2anc 583 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
208206, 207sge0xrcl 45745 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ*)
209206, 207sge0ge0 45744 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 0 ≤ (Σ^‘(𝑘𝐵𝐶)))
210203, 205, 35syl2anc 583 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
211 ltpnf 13126 . . . . . . . . 9 ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ → (Σ^‘(𝑘𝐵𝐶)) < +∞)
212210, 211syl 17 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) < +∞)
213200, 202, 208, 209, 212elicod 13400 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
214198, 213sge0fsummpt 45750 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑥𝑦^‘(𝑘𝐵𝐶)))
215196, 214eqtrd 2767 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) = Σ𝑥𝑦^‘(𝑘𝐵𝐶)))
216 nfv 1910 . . . . . 6 𝑘(𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin))
217189adantr 480 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥𝐴 𝐵 ∈ V)
218190fvmptelcdm 7117 . . . . . . 7 ((𝜑𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
219218adantlr 714 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
220198, 210fsumrecl 15706 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ)
221220rexrd 11288 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ*)
222 nfv 1910 . . . . . . . 8 𝑘((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+)
223 iunss1 5005 . . . . . . . . . . . 12 (𝑦𝐴 𝑥𝑦 𝐵 𝑥𝐴 𝐵)
224193, 223syl 17 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥𝑦 𝐵 𝑥𝐴 𝐵)
225224adantl 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥𝑦 𝐵 𝑥𝐴 𝐵)
226217, 225ssexd 5318 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥𝑦 𝐵 ∈ V)
227226adantr 480 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → 𝑥𝑦 𝐵 ∈ V)
228 simpll 766 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝜑)
229225sselda 3978 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝑘 𝑥𝐴 𝐵)
230228, 229, 218syl2anc 583 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
231230adantlr 714 . . . . . . . 8 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑘 𝑥𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
232 simpr 484 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → 𝑝 ∈ ℝ+)
233193adantl 481 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦𝐴)
23457adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Disj 𝑥𝐴 𝐵)
235 disjss1 5113 . . . . . . . . . . . 12 (𝑦𝐴 → (Disj 𝑥𝐴 𝐵Disj 𝑥𝑦 𝐵))
236233, 234, 235sylc 65 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Disj 𝑥𝑦 𝐵)
2372033adant3 1130 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝜑)
2382053adant3 1130 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝑥𝐴)
239 simp3 1136 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝑘𝐵)
240237, 238, 239, 25syl3anc 1369 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
241198, 206, 236, 240, 210sge0iunmptlemfi 45773 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))))
242214, 220eqeltrd 2828 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ∈ ℝ)
243241, 242eqeltrd 2828 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) ∈ ℝ)
244243adantr 480 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) ∈ ℝ)
245222, 227, 231, 232, 244sge0ltfirpmpt 45768 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → ∃𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)(Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
246 nfv 1910 . . . . . . . 8 𝑏((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+)
247 nfre1 3277 . . . . . . . 8 𝑏𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝)
248223sspwd 4611 . . . . . . . . . . . . . . . 16 (𝑦𝐴 → 𝒫 𝑥𝑦 𝐵 ⊆ 𝒫 𝑥𝐴 𝐵)
249193, 248syl 17 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝒫 𝑥𝑦 𝐵 ⊆ 𝒫 𝑥𝐴 𝐵)
250249adantr 480 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝒫 𝑥𝑦 𝐵 ⊆ 𝒫 𝑥𝐴 𝐵)
251 elinel1 4191 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → 𝑏 ∈ 𝒫 𝑥𝑦 𝐵)
252251adantl 481 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 𝑥𝑦 𝐵)
253250, 252sseldd 3979 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 𝑥𝐴 𝐵)
254 elinel2 4192 . . . . . . . . . . . . . 14 (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → 𝑏 ∈ Fin)
255254adantl 481 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ Fin)
256253, 255elind 4190 . . . . . . . . . . . 12 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
257256ad4ant24 753 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
2582573adant3 1130 . . . . . . . . . 10 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → 𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
259221ad2antrr 725 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ*)
2602593adant3 1130 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ*)
261 nfv 1910 . . . . . . . . . . . . . . . 16 𝑘((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin))
262226adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑥𝑦 𝐵 ∈ V)
263230adantlr 714 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
264243adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) ∈ ℝ)
265251elpwid 4607 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → 𝑏 𝑥𝑦 𝐵)
266265adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 𝑥𝑦 𝐵)
267261, 262, 263, 264, 266sge0ssrempt 45765 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ)
268267rexrd 11288 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ*)
269268adantlr 714 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ*)
270 rpxr 13009 . . . . . . . . . . . . . 14 (𝑝 ∈ ℝ+𝑝 ∈ ℝ*)
271270ad2antlr 726 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ*)
272269, 271xaddcld 13306 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) ∈ ℝ*)
2732723adant3 1130 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) ∈ ℝ*)
274 simp3 1136 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
275241, 214eqtr2d 2768 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)))
276275adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)))
2772763ad2ant1 1131 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)))
278267adantlr 714 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ)
279 rpre 13008 . . . . . . . . . . . . . . . 16 (𝑝 ∈ ℝ+𝑝 ∈ ℝ)
280279ad2antlr 726 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ)
281 rexadd 13237 . . . . . . . . . . . . . . 15 (((Σ^‘(𝑘𝑏𝐶)) ∈ ℝ ∧ 𝑝 ∈ ℝ) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) = ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
282278, 280, 281syl2anc 583 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) = ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
2832823adant3 1130 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) = ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
284277, 283breq12d 5155 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → (Σ𝑥𝑦^‘(𝑘𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) ↔ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)))
285274, 284mpbird 257 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
286260, 273, 285xrltled 13155 . . . . . . . . . 10 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
287 rspe 3241 . . . . . . . . . 10 ((𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) ∧ Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝)) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
288258, 286, 287syl2anc 583 . . . . . . . . 9 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
2892883exp 1117 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))))
290246, 247, 289rexlimd 3258 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → (∃𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)(Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝)))
291245, 290mpd 15 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
292216, 217, 219, 221, 291sge0gerpmpt 45762 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
293215, 292eqbrtrd 5164 . . . 4 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
294293ralrimiva 3141 . . 3 (𝜑 → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
295 eqid 2727 . . . . 5 (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))
296179, 295fmptd 7118 . . . 4 (𝜑 → (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))):𝐴⟶(0[,]+∞))
297132, 296, 1sge0lefi 45758 . . 3 (𝜑 → ((Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ↔ ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶))))
298294, 297mpbird 257 . 2 (𝜑 → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
2991, 2, 192, 298xrletrid 13160 1 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1085   = wceq 1534  wcel 2099  wne 2935  wral 3056  wrex 3065  {crab 3427  Vcvv 3469  csb 3889  cin 3943  wss 3944  c0 4318  𝒫 cpw 4598   ciun 4991  Disj wdisj 5107   class class class wbr 5142  cmpt 5225  cres 5674  wf 6538  cfv 6542  (class class class)co 7414  Fincfn 8957  cc 11130  cr 11131  0cc0 11132   + caddc 11135  +∞cpnf 11269  *cxr 11271   < clt 11272  cle 11273  +crp 13000   +𝑒 cxad 13116  [,)cico 13352  [,]cicc 13353  Σcsu 15658  Σ^csumge0 45722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9658  ax-ac2 10480  ax-cnex 11188  ax-resscn 11189  ax-1cn 11190  ax-icn 11191  ax-addcl 11192  ax-addrcl 11193  ax-mulcl 11194  ax-mulrcl 11195  ax-mulcom 11196  ax-addass 11197  ax-mulass 11198  ax-distr 11199  ax-i2m1 11200  ax-1ne0 11201  ax-1rid 11202  ax-rnegex 11203  ax-rrecex 11204  ax-cnre 11205  ax-pre-lttri 11206  ax-pre-lttrn 11207  ax-pre-ltadd 11208  ax-pre-mulgt0 11209  ax-pre-sup 11210
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-disj 5108  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-map 8840  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-sup 9459  df-oi 9527  df-card 9956  df-acn 9959  df-ac 10133  df-pnf 11274  df-mnf 11275  df-xr 11276  df-ltxr 11277  df-le 11278  df-sub 11470  df-neg 11471  df-div 11896  df-nn 12237  df-2 12299  df-3 12300  df-n0 12497  df-z 12583  df-uz 12847  df-rp 13001  df-xadd 13119  df-ico 13356  df-icc 13357  df-fz 13511  df-fzo 13654  df-seq 13993  df-exp 14053  df-hash 14316  df-cj 15072  df-re 15073  df-im 15074  df-sqrt 15208  df-abs 15209  df-clim 15458  df-sum 15659  df-sumge0 45723
This theorem is referenced by:  sge0iunmpt  45778
  Copyright terms: Public domain W3C validator