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 46430
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 45054 . . . . . . . . . 10 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → 𝑦 𝑥𝐴 𝐵)
43resmptd 6058 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → ((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦) = (𝑘𝑦𝐶))
54fveq2d 6910 . . . . . . . 8 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = (Σ^‘(𝑘𝑦𝐶)))
65adantl 481 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = (Σ^‘(𝑘𝑦𝐶)))
7 elinel2 4202 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
87adantl 481 . . . . . . . 8 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → 𝑦 ∈ Fin)
93sselda 3983 . . . . . . . . . . 11 ((𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) ∧ 𝑘𝑦) → 𝑘 𝑥𝐴 𝐵)
10 eliun 4995 . . . . . . . . . . 11 (𝑘 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑘𝐵)
119, 10sylib 218 . . . . . . . . . 10 ((𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) ∧ 𝑘𝑦) → ∃𝑥𝐴 𝑘𝐵)
1211adantll 714 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → ∃𝑥𝐴 𝑘𝐵)
13 nfv 1914 . . . . . . . . . . . 12 𝑥𝜑
14 nfcv 2905 . . . . . . . . . . . . 13 𝑥𝑦
15 nfiu1 5027 . . . . . . . . . . . . . . 15 𝑥 𝑥𝐴 𝐵
1615nfpw 4619 . . . . . . . . . . . . . 14 𝑥𝒫 𝑥𝐴 𝐵
17 nfcv 2905 . . . . . . . . . . . . . 14 𝑥Fin
1816, 17nfin 4224 . . . . . . . . . . . . 13 𝑥(𝒫 𝑥𝐴 𝐵 ∩ Fin)
1914, 18nfel 2920 . . . . . . . . . . . 12 𝑥 𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)
2013, 19nfan 1899 . . . . . . . . . . 11 𝑥(𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
21 nfv 1914 . . . . . . . . . . 11 𝑥 𝑘𝑦
2220, 21nfan 1899 . . . . . . . . . 10 𝑥((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦)
23 nfv 1914 . . . . . . . . . 10 𝑥 𝐶 ∈ (0[,)+∞)
24 simp3 1139 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → 𝑘𝐵)
25 sge0iunmptlemre.c . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
26 eqid 2737 . . . . . . . . . . . . . . . 16 (𝑘𝐵𝐶) = (𝑘𝐵𝐶)
2726fvmpt2 7027 . . . . . . . . . . . . . . 15 ((𝑘𝐵𝐶 ∈ (0[,]+∞)) → ((𝑘𝐵𝐶)‘𝑘) = 𝐶)
2824, 25, 27syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → ((𝑘𝐵𝐶)‘𝑘) = 𝐶)
2928eqcomd 2743 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 = ((𝑘𝐵𝐶)‘𝑘))
30253expa 1119 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
3130, 26fmptd 7134 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
32313adant3 1133 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
33 sge0iunmptlemre.b . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → 𝐵𝑊)
34333adant3 1133 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴𝑘𝐵) → 𝐵𝑊)
35 sge0iunmptlemre.re . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
36353adant3 1133 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴𝑘𝐵) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
3734, 32, 36sge0rern 46403 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → ¬ +∞ ∈ ran (𝑘𝐵𝐶))
3832, 37fge0iccico 46385 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → (𝑘𝐵𝐶):𝐵⟶(0[,)+∞))
3938, 24ffvelcdmd 7105 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴𝑘𝐵) → ((𝑘𝐵𝐶)‘𝑘) ∈ (0[,)+∞))
4029, 39eqeltrd 2841 . . . . . . . . . . . 12 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,)+∞))
41403exp 1120 . . . . . . . . . . 11 (𝜑 → (𝑥𝐴 → (𝑘𝐵𝐶 ∈ (0[,)+∞))))
4241ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → (𝑥𝐴 → (𝑘𝐵𝐶 ∈ (0[,)+∞))))
4322, 23, 42rexlimd 3266 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → (∃𝑥𝐴 𝑘𝐵𝐶 ∈ (0[,)+∞)))
4412, 43mpd 15 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → 𝐶 ∈ (0[,)+∞))
458, 44sge0fsummpt 46405 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑦𝐶)) = Σ𝑘𝑦 𝐶)
46 sseqin2 4223 . . . . . . . . . . . . . 14 (𝑦 𝑥𝐴 𝐵 ↔ ( 𝑥𝐴 𝐵𝑦) = 𝑦)
4746biimpi 216 . . . . . . . . . . . . 13 (𝑦 𝑥𝐴 𝐵 → ( 𝑥𝐴 𝐵𝑦) = 𝑦)
4847eqcomd 2743 . . . . . . . . . . . 12 (𝑦 𝑥𝐴 𝐵𝑦 = ( 𝑥𝐴 𝐵𝑦))
49 iunin1 5072 . . . . . . . . . . . . 13 𝑥𝐴 (𝐵𝑦) = ( 𝑥𝐴 𝐵𝑦)
5049a1i 11 . . . . . . . . . . . 12 (𝑦 𝑥𝐴 𝐵 𝑥𝐴 (𝐵𝑦) = ( 𝑥𝐴 𝐵𝑦))
5148, 50eqtr4d 2780 . . . . . . . . . . 11 (𝑦 𝑥𝐴 𝐵𝑦 = 𝑥𝐴 (𝐵𝑦))
523, 51syl 17 . . . . . . . . . 10 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → 𝑦 = 𝑥𝐴 (𝐵𝑦))
5352sumeq1d 15736 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → Σ𝑘𝑦 𝐶 = Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶)
5453adantl 481 . . . . . . . 8 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑘𝑦 𝐶 = Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶)
55 simpl 482 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → 𝜑)
5633adantlr 715 . . . . . . . . . 10 (((𝜑𝑦 ∈ Fin) ∧ 𝑥𝐴) → 𝐵𝑊)
57 sge0iunmptlemre.dj . . . . . . . . . . 11 (𝜑Disj 𝑥𝐴 𝐵)
5857adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → Disj 𝑥𝐴 𝐵)
59 rge0ssre 13496 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ ℝ
60 ax-resscn 11212 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
6159, 60sstri 3993 . . . . . . . . . . . 12 (0[,)+∞) ⊆ ℂ
6261, 40sselid 3981 . . . . . . . . . . 11 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ ℂ)
63623adant1r 1178 . . . . . . . . . 10 (((𝜑𝑦 ∈ Fin) ∧ 𝑥𝐴𝑘𝐵) → 𝐶 ∈ ℂ)
64 simpr 484 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → 𝑦 ∈ Fin)
6556, 58, 63, 64fsumiunss 45590 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶 = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
6655, 8, 65syl2anc 584 . . . . . . . 8 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶 = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
6754, 66eqtrd 2777 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑘𝑦 𝐶 = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
686, 45, 673eqtrd 2781 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
6956, 58, 64disjinfi 45197 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ∈ Fin)
70 id 22 . . . . . . . . . . . . 13 (𝑦 ∈ Fin → 𝑦 ∈ Fin)
71 inss2 4238 . . . . . . . . . . . . . 14 (𝑤 / 𝑥𝐵𝑦) ⊆ 𝑦
7271a1i 11 . . . . . . . . . . . . 13 (𝑦 ∈ Fin → (𝑤 / 𝑥𝐵𝑦) ⊆ 𝑦)
73 ssfi 9213 . . . . . . . . . . . . 13 ((𝑦 ∈ Fin ∧ (𝑤 / 𝑥𝐵𝑦) ⊆ 𝑦) → (𝑤 / 𝑥𝐵𝑦) ∈ Fin)
7470, 72, 73syl2anc 584 . . . . . . . . . . . 12 (𝑦 ∈ Fin → (𝑤 / 𝑥𝐵𝑦) ∈ Fin)
7574ad2antlr 727 . . . . . . . . . . 11 (((𝜑𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (𝑤 / 𝑥𝐵𝑦) ∈ Fin)
76 simpll 767 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝜑)
77 elrabi 3687 . . . . . . . . . . . . . 14 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} → 𝑤𝐴)
7877ad2antlr 727 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑤𝐴)
79 elinel1 4201 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) → 𝑘𝑤 / 𝑥𝐵)
8079adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑘𝑤 / 𝑥𝐵)
81 nfv 1914 . . . . . . . . . . . . . . . 16 𝑥 𝑤𝐴
82 nfcv 2905 . . . . . . . . . . . . . . . . 17 𝑥𝑘
83 nfcsb1v 3923 . . . . . . . . . . . . . . . . 17 𝑥𝑤 / 𝑥𝐵
8482, 83nfel 2920 . . . . . . . . . . . . . . . 16 𝑥 𝑘𝑤 / 𝑥𝐵
8513, 81, 84nf3an 1901 . . . . . . . . . . . . . . 15 𝑥(𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵)
8685, 23nfim 1896 . . . . . . . . . . . . . 14 𝑥((𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵) → 𝐶 ∈ (0[,)+∞))
87 eleq1w 2824 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
88 csbeq1a 3913 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
8988eleq2d 2827 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑘𝐵𝑘𝑤 / 𝑥𝐵))
9087, 893anbi23d 1441 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → ((𝜑𝑥𝐴𝑘𝐵) ↔ (𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵)))
9190imbi1d 341 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,)+∞)) ↔ ((𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵) → 𝐶 ∈ (0[,)+∞))))
9286, 91, 40chvarfv 2240 . . . . . . . . . . . . 13 ((𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵) → 𝐶 ∈ (0[,)+∞))
9376, 78, 80, 92syl3anc 1373 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
9493adantllr 719 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
9575, 94fsumge0cl 45588 . . . . . . . . . 10 (((𝜑𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶 ∈ (0[,)+∞))
9669, 95sge0fsummpt 46405 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)) = Σ𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
97 inss2 4238 . . . . . . . . . . . . . . . . 17 (𝐵𝑦) ⊆ 𝑦
9897a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ Fin → (𝐵𝑦) ⊆ 𝑦)
99 ssfi 9213 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ Fin ∧ (𝐵𝑦) ⊆ 𝑦) → (𝐵𝑦) ∈ Fin)
10070, 98, 99syl2anc 584 . . . . . . . . . . . . . . 15 (𝑦 ∈ Fin → (𝐵𝑦) ∈ Fin)
101100ad2antlr 727 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (𝐵𝑦) ∈ Fin)
102 simpll 767 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝜑)
103 rabid 3458 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↔ (𝑥𝐴 ∧ (𝐵𝑦) ≠ ∅))
104103biimpi 216 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} → (𝑥𝐴 ∧ (𝐵𝑦) ≠ ∅))
105104simpld 494 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} → 𝑥𝐴)
106105ad2antlr 727 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝑥𝐴)
107 elinel1 4201 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (𝐵𝑦) → 𝑘𝐵)
108107adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝑘𝐵)
109102, 106, 108, 40syl3anc 1373 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
110109adantllr 719 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
111101, 110sge0fsummpt 46405 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) = Σ𝑘 ∈ (𝐵𝑦)𝐶)
112111mpteq2dva 5242 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ Fin) → (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))) = (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵𝑦)𝐶))
113 nfrab1 3457 . . . . . . . . . . . . . 14 𝑥{𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}
114 nfcv 2905 . . . . . . . . . . . . . 14 𝑤{𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}
115 nfcv 2905 . . . . . . . . . . . . . 14 𝑤Σ𝑘 ∈ (𝐵𝑦)𝐶
11683, 14nfin 4224 . . . . . . . . . . . . . . 15 𝑥(𝑤 / 𝑥𝐵𝑦)
117 nfcv 2905 . . . . . . . . . . . . . . 15 𝑥𝐶
118116, 117nfsum 15727 . . . . . . . . . . . . . 14 𝑥Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶
11988ineq1d 4219 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝐵𝑦) = (𝑤 / 𝑥𝐵𝑦))
120119sumeq1d 15736 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → Σ𝑘 ∈ (𝐵𝑦)𝐶 = Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
121113, 114, 115, 118, 120cbvmptf 5251 . . . . . . . . . . . . 13 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵𝑦)𝐶) = (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
122121a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ Fin) → (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵𝑦)𝐶) = (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶))
123112, 122eqtr2d 2778 . . . . . . . . . . 11 ((𝜑𝑦 ∈ Fin) → (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶) = (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))))
124123fveq2d 6910 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)) = (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
125124eqcomd 2743 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)))
126120, 115, 118cbvsum 15731 . . . . . . . . . 10 Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶 = Σ𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶
127126a1i 11 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶 = Σ𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
12896, 125, 1273eqtr4d 2787 . . . . . . . 8 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
12955, 8, 128syl2anc 584 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
130129eqcomd 2743 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶 = (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
13168, 130eqtrd 2777 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
132 sge0iunmptlemre.a . . . . . . . . 9 (𝜑𝐴𝑉)
13377ssriv 3987 . . . . . . . . . 10 {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ⊆ 𝐴
134133a1i 11 . . . . . . . . 9 (𝜑 → {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ⊆ 𝐴)
135132, 134ssexd 5324 . . . . . . . 8 (𝜑 → {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ∈ V)
136 vex 3484 . . . . . . . . . . . . 13 𝑦 ∈ V
137136inex2 5318 . . . . . . . . . . . 12 (𝑤 / 𝑥𝐵𝑦) ∈ V
138137a1i 11 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (𝑤 / 𝑥𝐵𝑦) ∈ V)
139 icossicc 13476 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ (0[,]+∞)
140 simpll 767 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝜑)
141 simplr 769 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑤𝐴)
14279adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑘𝑤 / 𝑥𝐵)
143140, 141, 142, 92syl3anc 1373 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
144139, 143sselid 3981 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,]+∞))
145 eqid 2737 . . . . . . . . . . . 12 (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶) = (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)
146144, 145fmptd 7134 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶):(𝑤 / 𝑥𝐵𝑦)⟶(0[,]+∞))
147138, 146sge0cl 46396 . . . . . . . . . 10 ((𝜑𝑤𝐴) → (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
14877, 147sylan2 593 . . . . . . . . 9 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
149 nfcv 2905 . . . . . . . . . 10 𝑤^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))
150 nfcv 2905 . . . . . . . . . . 11 𝑥Σ^
151116, 117nfmpt 5249 . . . . . . . . . . 11 𝑥(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)
152150, 151nffv 6916 . . . . . . . . . 10 𝑥^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))
153119mpteq1d 5237 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑘 ∈ (𝐵𝑦) ↦ 𝐶) = (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))
154153fveq2d 6910 . . . . . . . . . 10 (𝑥 = 𝑤 → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) = (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
155113, 114, 149, 152, 154cbvmptf 5251 . . . . . . . . 9 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))) = (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
156148, 155fmptd 7134 . . . . . . . 8 (𝜑 → (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))):{𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}⟶(0[,]+∞))
157135, 156sge0xrcl 46400 . . . . . . 7 (𝜑 → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
158157adantr 480 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
159 eqid 2737 . . . . . . . . 9 (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))) = (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
160147, 159fmptd 7134 . . . . . . . 8 (𝜑 → (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))):𝐴⟶(0[,]+∞))
161132, 160sge0xrcl 46400 . . . . . . 7 (𝜑 → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
162161adantr 480 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
16355, 2syl 17 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ∈ ℝ*)
164155fveq2i 6909 . . . . . . . . 9 ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))))
165164a1i 11 . . . . . . . 8 (𝜑 → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
166132, 147, 134sge0lessmpt 46414 . . . . . . . 8 (𝜑 → (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
167165, 166eqbrtrd 5165 . . . . . . 7 (𝜑 → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
168167adantr 480 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
169149, 152, 154cbvmpt 5253 . . . . . . . . . . 11 (𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))) = (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
170169eqcomi 2746 . . . . . . . . . 10 (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))
171170fveq2i 6909 . . . . . . . . 9 ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))))
172171a1i 11 . . . . . . . 8 (𝜑 → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
173136inex2 5318 . . . . . . . . . . 11 (𝐵𝑦) ∈ V
174173a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐵𝑦) ∈ V)
175107, 30sylan2 593 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝐶 ∈ (0[,]+∞))
176 eqid 2737 . . . . . . . . . . 11 (𝑘 ∈ (𝐵𝑦) ↦ 𝐶) = (𝑘 ∈ (𝐵𝑦) ↦ 𝐶)
177175, 176fmptd 7134 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑘 ∈ (𝐵𝑦) ↦ 𝐶):(𝐵𝑦)⟶(0[,]+∞))
178174, 177sge0cl 46396 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
17933, 31sge0cl 46396 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,]+∞))
180 inss1 4237 . . . . . . . . . . 11 (𝐵𝑦) ⊆ 𝐵
181180a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐵𝑦) ⊆ 𝐵)
18233, 30, 181sge0lessmpt 46414 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) ≤ (Σ^‘(𝑘𝐵𝐶)))
18313, 132, 178, 179, 182sge0lempt 46425 . . . . . . . 8 (𝜑 → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
184172, 183eqbrtrd 5165 . . . . . . 7 (𝜑 → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
185184adantr 480 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
186158, 162, 163, 168, 185xrletrd 13204 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
187131, 186eqbrtrd 5165 . . . 4 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
188187ralrimiva 3146 . . 3 (𝜑 → ∀𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)(Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
189 sge0iunmptlemre.iue . . . 4 (𝜑 𝑥𝐴 𝐵 ∈ V)
190 sge0iunmptlemre.f . . . 4 (𝜑 → (𝑘 𝑥𝐴 𝐵𝐶): 𝑥𝐴 𝐵⟶(0[,]+∞))
191189, 190, 2sge0lefi 46413 . . 3 (𝜑 → ((Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ ∀𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)(Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))))
192188, 191mpbird 257 . 2 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
193 elpwinss 45054 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦𝐴)
194193resmptd 6058 . . . . . . . 8 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → ((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦) = (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))))
195194fveq2d 6910 . . . . . . 7 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))))
196195adantl 481 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))))
197 elinel2 4202 . . . . . . . 8 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
198197adantl 481 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin)
199 0xr 11308 . . . . . . . . 9 0 ∈ ℝ*
200199a1i 11 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 0 ∈ ℝ*)
201 pnfxr 11315 . . . . . . . . 9 +∞ ∈ ℝ*
202201a1i 11 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → +∞ ∈ ℝ*)
203 simpll 767 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 𝜑)
204193sselda 3983 . . . . . . . . . . 11 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑥𝑦) → 𝑥𝐴)
205204adantll 714 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 𝑥𝐴)
206203, 205, 33syl2anc 584 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 𝐵𝑊)
207203, 205, 31syl2anc 584 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
208206, 207sge0xrcl 46400 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ*)
209206, 207sge0ge0 46399 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 0 ≤ (Σ^‘(𝑘𝐵𝐶)))
210203, 205, 35syl2anc 584 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
211 ltpnf 13162 . . . . . . . . 9 ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ → (Σ^‘(𝑘𝐵𝐶)) < +∞)
212210, 211syl 17 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) < +∞)
213200, 202, 208, 209, 212elicod 13437 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
214198, 213sge0fsummpt 46405 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑥𝑦^‘(𝑘𝐵𝐶)))
215196, 214eqtrd 2777 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) = Σ𝑥𝑦^‘(𝑘𝐵𝐶)))
216 nfv 1914 . . . . . 6 𝑘(𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin))
217189adantr 480 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥𝐴 𝐵 ∈ V)
218190fvmptelcdm 7133 . . . . . . 7 ((𝜑𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
219218adantlr 715 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
220198, 210fsumrecl 15770 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ)
221220rexrd 11311 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ*)
222 nfv 1914 . . . . . . . 8 𝑘((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+)
223 iunss1 5006 . . . . . . . . . . . 12 (𝑦𝐴 𝑥𝑦 𝐵 𝑥𝐴 𝐵)
224193, 223syl 17 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥𝑦 𝐵 𝑥𝐴 𝐵)
225224adantl 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥𝑦 𝐵 𝑥𝐴 𝐵)
226217, 225ssexd 5324 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥𝑦 𝐵 ∈ V)
227226adantr 480 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → 𝑥𝑦 𝐵 ∈ V)
228 simpll 767 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝜑)
229225sselda 3983 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝑘 𝑥𝐴 𝐵)
230228, 229, 218syl2anc 584 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
231230adantlr 715 . . . . . . . 8 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑘 𝑥𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
232 simpr 484 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → 𝑝 ∈ ℝ+)
233193adantl 481 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦𝐴)
23457adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Disj 𝑥𝐴 𝐵)
235 disjss1 5116 . . . . . . . . . . . 12 (𝑦𝐴 → (Disj 𝑥𝐴 𝐵Disj 𝑥𝑦 𝐵))
236233, 234, 235sylc 65 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Disj 𝑥𝑦 𝐵)
2372033adant3 1133 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝜑)
2382053adant3 1133 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝑥𝐴)
239 simp3 1139 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝑘𝐵)
240237, 238, 239, 25syl3anc 1373 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
241198, 206, 236, 240, 210sge0iunmptlemfi 46428 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))))
242214, 220eqeltrd 2841 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ∈ ℝ)
243241, 242eqeltrd 2841 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) ∈ ℝ)
244243adantr 480 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) ∈ ℝ)
245222, 227, 231, 232, 244sge0ltfirpmpt 46423 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → ∃𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)(Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
246 nfv 1914 . . . . . . . 8 𝑏((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+)
247 nfre1 3285 . . . . . . . 8 𝑏𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝)
248223sspwd 4613 . . . . . . . . . . . . . . . 16 (𝑦𝐴 → 𝒫 𝑥𝑦 𝐵 ⊆ 𝒫 𝑥𝐴 𝐵)
249193, 248syl 17 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝒫 𝑥𝑦 𝐵 ⊆ 𝒫 𝑥𝐴 𝐵)
250249adantr 480 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝒫 𝑥𝑦 𝐵 ⊆ 𝒫 𝑥𝐴 𝐵)
251 elinel1 4201 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → 𝑏 ∈ 𝒫 𝑥𝑦 𝐵)
252251adantl 481 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 𝑥𝑦 𝐵)
253250, 252sseldd 3984 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 𝑥𝐴 𝐵)
254 elinel2 4202 . . . . . . . . . . . . . 14 (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → 𝑏 ∈ Fin)
255254adantl 481 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ Fin)
256253, 255elind 4200 . . . . . . . . . . . 12 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
257256ad4ant24 754 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
2582573adant3 1133 . . . . . . . . . 10 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → 𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
259221ad2antrr 726 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ*)
2602593adant3 1133 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ*)
261 nfv 1914 . . . . . . . . . . . . . . . 16 𝑘((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin))
262226adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑥𝑦 𝐵 ∈ V)
263230adantlr 715 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
264243adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) ∈ ℝ)
265251elpwid 4609 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → 𝑏 𝑥𝑦 𝐵)
266265adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 𝑥𝑦 𝐵)
267261, 262, 263, 264, 266sge0ssrempt 46420 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ)
268267rexrd 11311 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ*)
269268adantlr 715 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ*)
270 rpxr 13044 . . . . . . . . . . . . . 14 (𝑝 ∈ ℝ+𝑝 ∈ ℝ*)
271270ad2antlr 727 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ*)
272269, 271xaddcld 13343 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) ∈ ℝ*)
2732723adant3 1133 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) ∈ ℝ*)
274 simp3 1139 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
275241, 214eqtr2d 2778 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)))
276275adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)))
2772763ad2ant1 1134 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)))
278267adantlr 715 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ)
279 rpre 13043 . . . . . . . . . . . . . . . 16 (𝑝 ∈ ℝ+𝑝 ∈ ℝ)
280279ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ)
281 rexadd 13274 . . . . . . . . . . . . . . 15 (((Σ^‘(𝑘𝑏𝐶)) ∈ ℝ ∧ 𝑝 ∈ ℝ) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) = ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
282278, 280, 281syl2anc 584 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) = ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
2832823adant3 1133 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) = ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
284277, 283breq12d 5156 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → (Σ𝑥𝑦^‘(𝑘𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) ↔ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)))
285274, 284mpbird 257 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
286260, 273, 285xrltled 13192 . . . . . . . . . 10 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
287 rspe 3249 . . . . . . . . . 10 ((𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) ∧ Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝)) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
288258, 286, 287syl2anc 584 . . . . . . . . 9 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
2892883exp 1120 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))))
290246, 247, 289rexlimd 3266 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → (∃𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)(Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝)))
291245, 290mpd 15 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
292216, 217, 219, 221, 291sge0gerpmpt 46417 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
293215, 292eqbrtrd 5165 . . . 4 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
294293ralrimiva 3146 . . 3 (𝜑 → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
295 eqid 2737 . . . . 5 (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))
296179, 295fmptd 7134 . . . 4 (𝜑 → (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))):𝐴⟶(0[,]+∞))
297132, 296, 1sge0lefi 46413 . . 3 (𝜑 → ((Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ↔ ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶))))
298294, 297mpbird 257 . 2 (𝜑 → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
2991, 2, 192, 298xrletrid 13197 1 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  csb 3899  cin 3950  wss 3951  c0 4333  𝒫 cpw 4600   ciun 4991  Disj wdisj 5110   class class class wbr 5143  cmpt 5225  cres 5687  wf 6557  cfv 6561  (class class class)co 7431  Fincfn 8985  cc 11153  cr 11154  0cc0 11155   + caddc 11158  +∞cpnf 11292  *cxr 11294   < clt 11295  cle 11296  +crp 13034   +𝑒 cxad 13152  [,)cico 13389  [,]cicc 13390  Σcsu 15722  Σ^csumge0 46377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-ac2 10503  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-oi 9550  df-card 9979  df-acn 9982  df-ac 10156  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-rp 13035  df-xadd 13155  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-sumge0 46378
This theorem is referenced by:  sge0iunmpt  46433
  Copyright terms: Public domain W3C validator