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 43924
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 42567 . . . . . . . . . 10 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → 𝑦 𝑥𝐴 𝐵)
43resmptd 5947 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → ((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦) = (𝑘𝑦𝐶))
54fveq2d 6775 . . . . . . . 8 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = (Σ^‘(𝑘𝑦𝐶)))
65adantl 482 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = (Σ^‘(𝑘𝑦𝐶)))
7 elinel2 4135 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
87adantl 482 . . . . . . . 8 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → 𝑦 ∈ Fin)
93sselda 3926 . . . . . . . . . . 11 ((𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) ∧ 𝑘𝑦) → 𝑘 𝑥𝐴 𝐵)
10 eliun 4934 . . . . . . . . . . 11 (𝑘 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑘𝐵)
119, 10sylib 217 . . . . . . . . . 10 ((𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) ∧ 𝑘𝑦) → ∃𝑥𝐴 𝑘𝐵)
1211adantll 711 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → ∃𝑥𝐴 𝑘𝐵)
13 nfv 1921 . . . . . . . . . . . 12 𝑥𝜑
14 nfcv 2909 . . . . . . . . . . . . 13 𝑥𝑦
15 nfiu1 4964 . . . . . . . . . . . . . . 15 𝑥 𝑥𝐴 𝐵
1615nfpw 4560 . . . . . . . . . . . . . 14 𝑥𝒫 𝑥𝐴 𝐵
17 nfcv 2909 . . . . . . . . . . . . . 14 𝑥Fin
1816, 17nfin 4156 . . . . . . . . . . . . 13 𝑥(𝒫 𝑥𝐴 𝐵 ∩ Fin)
1914, 18nfel 2923 . . . . . . . . . . . 12 𝑥 𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)
2013, 19nfan 1906 . . . . . . . . . . 11 𝑥(𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
21 nfv 1921 . . . . . . . . . . 11 𝑥 𝑘𝑦
2220, 21nfan 1906 . . . . . . . . . 10 𝑥((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦)
23 nfv 1921 . . . . . . . . . 10 𝑥 𝐶 ∈ (0[,)+∞)
24 simp3 1137 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → 𝑘𝐵)
25 sge0iunmptlemre.c . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
26 eqid 2740 . . . . . . . . . . . . . . . 16 (𝑘𝐵𝐶) = (𝑘𝐵𝐶)
2726fvmpt2 6883 . . . . . . . . . . . . . . 15 ((𝑘𝐵𝐶 ∈ (0[,]+∞)) → ((𝑘𝐵𝐶)‘𝑘) = 𝐶)
2824, 25, 27syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → ((𝑘𝐵𝐶)‘𝑘) = 𝐶)
2928eqcomd 2746 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 = ((𝑘𝐵𝐶)‘𝑘))
30253expa 1117 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
3130, 26fmptd 6985 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
32313adant3 1131 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
33 sge0iunmptlemre.b . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → 𝐵𝑊)
34333adant3 1131 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴𝑘𝐵) → 𝐵𝑊)
35 sge0iunmptlemre.re . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
36353adant3 1131 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴𝑘𝐵) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
3734, 32, 36sge0rern 43897 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → ¬ +∞ ∈ ran (𝑘𝐵𝐶))
3832, 37fge0iccico 43879 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → (𝑘𝐵𝐶):𝐵⟶(0[,)+∞))
3938, 24ffvelrnd 6959 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴𝑘𝐵) → ((𝑘𝐵𝐶)‘𝑘) ∈ (0[,)+∞))
4029, 39eqeltrd 2841 . . . . . . . . . . . 12 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,)+∞))
41403exp 1118 . . . . . . . . . . 11 (𝜑 → (𝑥𝐴 → (𝑘𝐵𝐶 ∈ (0[,)+∞))))
4241ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → (𝑥𝐴 → (𝑘𝐵𝐶 ∈ (0[,)+∞))))
4322, 23, 42rexlimd 3248 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → (∃𝑥𝐴 𝑘𝐵𝐶 ∈ (0[,)+∞)))
4412, 43mpd 15 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → 𝐶 ∈ (0[,)+∞))
458, 44sge0fsummpt 43899 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑦𝐶)) = Σ𝑘𝑦 𝐶)
46 sseqin2 4155 . . . . . . . . . . . . . 14 (𝑦 𝑥𝐴 𝐵 ↔ ( 𝑥𝐴 𝐵𝑦) = 𝑦)
4746biimpi 215 . . . . . . . . . . . . 13 (𝑦 𝑥𝐴 𝐵 → ( 𝑥𝐴 𝐵𝑦) = 𝑦)
4847eqcomd 2746 . . . . . . . . . . . 12 (𝑦 𝑥𝐴 𝐵𝑦 = ( 𝑥𝐴 𝐵𝑦))
49 iunin1 5006 . . . . . . . . . . . . 13 𝑥𝐴 (𝐵𝑦) = ( 𝑥𝐴 𝐵𝑦)
5049a1i 11 . . . . . . . . . . . 12 (𝑦 𝑥𝐴 𝐵 𝑥𝐴 (𝐵𝑦) = ( 𝑥𝐴 𝐵𝑦))
5148, 50eqtr4d 2783 . . . . . . . . . . 11 (𝑦 𝑥𝐴 𝐵𝑦 = 𝑥𝐴 (𝐵𝑦))
523, 51syl 17 . . . . . . . . . 10 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → 𝑦 = 𝑥𝐴 (𝐵𝑦))
5352sumeq1d 15411 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → Σ𝑘𝑦 𝐶 = Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶)
5453adantl 482 . . . . . . . 8 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑘𝑦 𝐶 = Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶)
55 simpl 483 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → 𝜑)
5633adantlr 712 . . . . . . . . . 10 (((𝜑𝑦 ∈ Fin) ∧ 𝑥𝐴) → 𝐵𝑊)
57 sge0iunmptlemre.dj . . . . . . . . . . 11 (𝜑Disj 𝑥𝐴 𝐵)
5857adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → Disj 𝑥𝐴 𝐵)
59 rge0ssre 13187 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ ℝ
60 ax-resscn 10929 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
6159, 60sstri 3935 . . . . . . . . . . . 12 (0[,)+∞) ⊆ ℂ
6261, 40sselid 3924 . . . . . . . . . . 11 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ ℂ)
63623adant1r 1176 . . . . . . . . . 10 (((𝜑𝑦 ∈ Fin) ∧ 𝑥𝐴𝑘𝐵) → 𝐶 ∈ ℂ)
64 simpr 485 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → 𝑦 ∈ Fin)
6556, 58, 63, 64fsumiunss 43087 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶 = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
6655, 8, 65syl2anc 584 . . . . . . . 8 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶 = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
6754, 66eqtrd 2780 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑘𝑦 𝐶 = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
686, 45, 673eqtrd 2784 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
6956, 58, 64disjinfi 42701 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ∈ Fin)
70 id 22 . . . . . . . . . . . . 13 (𝑦 ∈ Fin → 𝑦 ∈ Fin)
71 inss2 4169 . . . . . . . . . . . . . 14 (𝑤 / 𝑥𝐵𝑦) ⊆ 𝑦
7271a1i 11 . . . . . . . . . . . . 13 (𝑦 ∈ Fin → (𝑤 / 𝑥𝐵𝑦) ⊆ 𝑦)
73 ssfi 8938 . . . . . . . . . . . . 13 ((𝑦 ∈ Fin ∧ (𝑤 / 𝑥𝐵𝑦) ⊆ 𝑦) → (𝑤 / 𝑥𝐵𝑦) ∈ Fin)
7470, 72, 73syl2anc 584 . . . . . . . . . . . 12 (𝑦 ∈ Fin → (𝑤 / 𝑥𝐵𝑦) ∈ Fin)
7574ad2antlr 724 . . . . . . . . . . 11 (((𝜑𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (𝑤 / 𝑥𝐵𝑦) ∈ Fin)
76 simpll 764 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝜑)
77 elrabi 3620 . . . . . . . . . . . . . 14 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} → 𝑤𝐴)
7877ad2antlr 724 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑤𝐴)
79 elinel1 4134 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) → 𝑘𝑤 / 𝑥𝐵)
8079adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑘𝑤 / 𝑥𝐵)
81 nfv 1921 . . . . . . . . . . . . . . . 16 𝑥 𝑤𝐴
82 nfcv 2909 . . . . . . . . . . . . . . . . 17 𝑥𝑘
83 nfcsb1v 3862 . . . . . . . . . . . . . . . . 17 𝑥𝑤 / 𝑥𝐵
8482, 83nfel 2923 . . . . . . . . . . . . . . . 16 𝑥 𝑘𝑤 / 𝑥𝐵
8513, 81, 84nf3an 1908 . . . . . . . . . . . . . . 15 𝑥(𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵)
8685, 23nfim 1903 . . . . . . . . . . . . . 14 𝑥((𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵) → 𝐶 ∈ (0[,)+∞))
87 eleq1w 2823 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
88 csbeq1a 3851 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
8988eleq2d 2826 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑘𝐵𝑘𝑤 / 𝑥𝐵))
9087, 893anbi23d 1438 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → ((𝜑𝑥𝐴𝑘𝐵) ↔ (𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵)))
9190imbi1d 342 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,)+∞)) ↔ ((𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵) → 𝐶 ∈ (0[,)+∞))))
9286, 91, 40chvarfv 2237 . . . . . . . . . . . . 13 ((𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵) → 𝐶 ∈ (0[,)+∞))
9376, 78, 80, 92syl3anc 1370 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
9493adantllr 716 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
9575, 94fsumge0cl 43085 . . . . . . . . . 10 (((𝜑𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶 ∈ (0[,)+∞))
9669, 95sge0fsummpt 43899 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)) = Σ𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
97 inss2 4169 . . . . . . . . . . . . . . . . 17 (𝐵𝑦) ⊆ 𝑦
9897a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ Fin → (𝐵𝑦) ⊆ 𝑦)
99 ssfi 8938 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ Fin ∧ (𝐵𝑦) ⊆ 𝑦) → (𝐵𝑦) ∈ Fin)
10070, 98, 99syl2anc 584 . . . . . . . . . . . . . . 15 (𝑦 ∈ Fin → (𝐵𝑦) ∈ Fin)
101100ad2antlr 724 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (𝐵𝑦) ∈ Fin)
102 simpll 764 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝜑)
103 rabid 3309 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↔ (𝑥𝐴 ∧ (𝐵𝑦) ≠ ∅))
104103biimpi 215 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} → (𝑥𝐴 ∧ (𝐵𝑦) ≠ ∅))
105104simpld 495 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} → 𝑥𝐴)
106105ad2antlr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝑥𝐴)
107 elinel1 4134 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (𝐵𝑦) → 𝑘𝐵)
108107adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝑘𝐵)
109102, 106, 108, 40syl3anc 1370 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
110109adantllr 716 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
111101, 110sge0fsummpt 43899 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) = Σ𝑘 ∈ (𝐵𝑦)𝐶)
112111mpteq2dva 5179 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ Fin) → (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))) = (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵𝑦)𝐶))
113 nfrab1 3316 . . . . . . . . . . . . . 14 𝑥{𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}
114 nfcv 2909 . . . . . . . . . . . . . 14 𝑤{𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}
115 nfcv 2909 . . . . . . . . . . . . . 14 𝑤Σ𝑘 ∈ (𝐵𝑦)𝐶
11683, 14nfin 4156 . . . . . . . . . . . . . . 15 𝑥(𝑤 / 𝑥𝐵𝑦)
117 nfcv 2909 . . . . . . . . . . . . . . 15 𝑥𝐶
118116, 117nfsum 15400 . . . . . . . . . . . . . 14 𝑥Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶
11988ineq1d 4151 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝐵𝑦) = (𝑤 / 𝑥𝐵𝑦))
120119sumeq1d 15411 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → Σ𝑘 ∈ (𝐵𝑦)𝐶 = Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
121113, 114, 115, 118, 120cbvmptf 5188 . . . . . . . . . . . . 13 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵𝑦)𝐶) = (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
122121a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ Fin) → (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵𝑦)𝐶) = (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶))
123112, 122eqtr2d 2781 . . . . . . . . . . 11 ((𝜑𝑦 ∈ Fin) → (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶) = (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))))
124123fveq2d 6775 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)) = (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
125124eqcomd 2746 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)))
126120, 114, 113, 115, 118cbvsum 15405 . . . . . . . . . 10 Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶 = Σ𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶
127126a1i 11 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶 = Σ𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
12896, 125, 1273eqtr4d 2790 . . . . . . . 8 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
12955, 8, 128syl2anc 584 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
130129eqcomd 2746 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶 = (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
13168, 130eqtrd 2780 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
132 sge0iunmptlemre.a . . . . . . . . 9 (𝜑𝐴𝑉)
13377ssriv 3930 . . . . . . . . . 10 {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ⊆ 𝐴
134133a1i 11 . . . . . . . . 9 (𝜑 → {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ⊆ 𝐴)
135132, 134ssexd 5252 . . . . . . . 8 (𝜑 → {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ∈ V)
136 vex 3435 . . . . . . . . . . . . 13 𝑦 ∈ V
137136inex2 5246 . . . . . . . . . . . 12 (𝑤 / 𝑥𝐵𝑦) ∈ V
138137a1i 11 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (𝑤 / 𝑥𝐵𝑦) ∈ V)
139 icossicc 13167 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ (0[,]+∞)
140 simpll 764 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝜑)
141 simplr 766 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑤𝐴)
14279adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑘𝑤 / 𝑥𝐵)
143140, 141, 142, 92syl3anc 1370 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
144139, 143sselid 3924 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,]+∞))
145 eqid 2740 . . . . . . . . . . . 12 (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶) = (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)
146144, 145fmptd 6985 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶):(𝑤 / 𝑥𝐵𝑦)⟶(0[,]+∞))
147138, 146sge0cl 43890 . . . . . . . . . 10 ((𝜑𝑤𝐴) → (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
14877, 147sylan2 593 . . . . . . . . 9 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
149 nfcv 2909 . . . . . . . . . 10 𝑤^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))
150 nfcv 2909 . . . . . . . . . . 11 𝑥Σ^
151116, 117nfmpt 5186 . . . . . . . . . . 11 𝑥(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)
152150, 151nffv 6781 . . . . . . . . . 10 𝑥^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))
153119mpteq1d 5174 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑘 ∈ (𝐵𝑦) ↦ 𝐶) = (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))
154153fveq2d 6775 . . . . . . . . . 10 (𝑥 = 𝑤 → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) = (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
155113, 114, 149, 152, 154cbvmptf 5188 . . . . . . . . 9 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))) = (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
156148, 155fmptd 6985 . . . . . . . 8 (𝜑 → (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))):{𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}⟶(0[,]+∞))
157135, 156sge0xrcl 43894 . . . . . . 7 (𝜑 → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
158157adantr 481 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
159 eqid 2740 . . . . . . . . 9 (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))) = (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
160147, 159fmptd 6985 . . . . . . . 8 (𝜑 → (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))):𝐴⟶(0[,]+∞))
161132, 160sge0xrcl 43894 . . . . . . 7 (𝜑 → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
162161adantr 481 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
16355, 2syl 17 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ∈ ℝ*)
164155fveq2i 6774 . . . . . . . . 9 ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))))
165164a1i 11 . . . . . . . 8 (𝜑 → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
166132, 147, 134sge0lessmpt 43908 . . . . . . . 8 (𝜑 → (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
167165, 166eqbrtrd 5101 . . . . . . 7 (𝜑 → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
168167adantr 481 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
169149, 152, 154cbvmpt 5190 . . . . . . . . . . 11 (𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))) = (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
170169eqcomi 2749 . . . . . . . . . 10 (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))
171170fveq2i 6774 . . . . . . . . 9 ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))))
172171a1i 11 . . . . . . . 8 (𝜑 → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
173136inex2 5246 . . . . . . . . . . 11 (𝐵𝑦) ∈ V
174173a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐵𝑦) ∈ V)
175107, 30sylan2 593 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝐶 ∈ (0[,]+∞))
176 eqid 2740 . . . . . . . . . . 11 (𝑘 ∈ (𝐵𝑦) ↦ 𝐶) = (𝑘 ∈ (𝐵𝑦) ↦ 𝐶)
177175, 176fmptd 6985 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑘 ∈ (𝐵𝑦) ↦ 𝐶):(𝐵𝑦)⟶(0[,]+∞))
178174, 177sge0cl 43890 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
17933, 31sge0cl 43890 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,]+∞))
180 inss1 4168 . . . . . . . . . . 11 (𝐵𝑦) ⊆ 𝐵
181180a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐵𝑦) ⊆ 𝐵)
18233, 30, 181sge0lessmpt 43908 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) ≤ (Σ^‘(𝑘𝐵𝐶)))
18313, 132, 178, 179, 182sge0lempt 43919 . . . . . . . 8 (𝜑 → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
184172, 183eqbrtrd 5101 . . . . . . 7 (𝜑 → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
185184adantr 481 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
186158, 162, 163, 168, 185xrletrd 12895 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
187131, 186eqbrtrd 5101 . . . 4 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
188187ralrimiva 3110 . . 3 (𝜑 → ∀𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)(Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
189 sge0iunmptlemre.iue . . . 4 (𝜑 𝑥𝐴 𝐵 ∈ V)
190 sge0iunmptlemre.f . . . 4 (𝜑 → (𝑘 𝑥𝐴 𝐵𝐶): 𝑥𝐴 𝐵⟶(0[,]+∞))
191189, 190, 2sge0lefi 43907 . . 3 (𝜑 → ((Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ ∀𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)(Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))))
192188, 191mpbird 256 . 2 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
193 elpwinss 42567 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦𝐴)
194193resmptd 5947 . . . . . . . 8 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → ((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦) = (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))))
195194fveq2d 6775 . . . . . . 7 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))))
196195adantl 482 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))))
197 elinel2 4135 . . . . . . . 8 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
198197adantl 482 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin)
199 0xr 11023 . . . . . . . . 9 0 ∈ ℝ*
200199a1i 11 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 0 ∈ ℝ*)
201 pnfxr 11030 . . . . . . . . 9 +∞ ∈ ℝ*
202201a1i 11 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → +∞ ∈ ℝ*)
203 simpll 764 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 𝜑)
204193sselda 3926 . . . . . . . . . . 11 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑥𝑦) → 𝑥𝐴)
205204adantll 711 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 𝑥𝐴)
206203, 205, 33syl2anc 584 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 𝐵𝑊)
207203, 205, 31syl2anc 584 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
208206, 207sge0xrcl 43894 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ*)
209206, 207sge0ge0 43893 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 0 ≤ (Σ^‘(𝑘𝐵𝐶)))
210203, 205, 35syl2anc 584 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
211 ltpnf 12855 . . . . . . . . 9 ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ → (Σ^‘(𝑘𝐵𝐶)) < +∞)
212210, 211syl 17 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) < +∞)
213200, 202, 208, 209, 212elicod 13128 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
214198, 213sge0fsummpt 43899 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑥𝑦^‘(𝑘𝐵𝐶)))
215196, 214eqtrd 2780 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) = Σ𝑥𝑦^‘(𝑘𝐵𝐶)))
216 nfv 1921 . . . . . 6 𝑘(𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin))
217189adantr 481 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥𝐴 𝐵 ∈ V)
218190fvmptelrn 6984 . . . . . . 7 ((𝜑𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
219218adantlr 712 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
220198, 210fsumrecl 15444 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ)
221220rexrd 11026 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ*)
222 nfv 1921 . . . . . . . 8 𝑘((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+)
223 iunss1 4944 . . . . . . . . . . . 12 (𝑦𝐴 𝑥𝑦 𝐵 𝑥𝐴 𝐵)
224193, 223syl 17 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥𝑦 𝐵 𝑥𝐴 𝐵)
225224adantl 482 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥𝑦 𝐵 𝑥𝐴 𝐵)
226217, 225ssexd 5252 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥𝑦 𝐵 ∈ V)
227226adantr 481 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → 𝑥𝑦 𝐵 ∈ V)
228 simpll 764 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝜑)
229225sselda 3926 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝑘 𝑥𝐴 𝐵)
230228, 229, 218syl2anc 584 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
231230adantlr 712 . . . . . . . 8 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑘 𝑥𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
232 simpr 485 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → 𝑝 ∈ ℝ+)
233193adantl 482 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦𝐴)
23457adantr 481 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Disj 𝑥𝐴 𝐵)
235 disjss1 5050 . . . . . . . . . . . 12 (𝑦𝐴 → (Disj 𝑥𝐴 𝐵Disj 𝑥𝑦 𝐵))
236233, 234, 235sylc 65 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Disj 𝑥𝑦 𝐵)
2372033adant3 1131 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝜑)
2382053adant3 1131 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝑥𝐴)
239 simp3 1137 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝑘𝐵)
240237, 238, 239, 25syl3anc 1370 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
241198, 206, 236, 240, 210sge0iunmptlemfi 43922 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))))
242214, 220eqeltrd 2841 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ∈ ℝ)
243241, 242eqeltrd 2841 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) ∈ ℝ)
244243adantr 481 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) ∈ ℝ)
245222, 227, 231, 232, 244sge0ltfirpmpt 43917 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → ∃𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)(Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
246 nfv 1921 . . . . . . . 8 𝑏((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+)
247 nfre1 3237 . . . . . . . 8 𝑏𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝)
248223sspwd 4554 . . . . . . . . . . . . . . . 16 (𝑦𝐴 → 𝒫 𝑥𝑦 𝐵 ⊆ 𝒫 𝑥𝐴 𝐵)
249193, 248syl 17 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝒫 𝑥𝑦 𝐵 ⊆ 𝒫 𝑥𝐴 𝐵)
250249adantr 481 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝒫 𝑥𝑦 𝐵 ⊆ 𝒫 𝑥𝐴 𝐵)
251 elinel1 4134 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → 𝑏 ∈ 𝒫 𝑥𝑦 𝐵)
252251adantl 482 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 𝑥𝑦 𝐵)
253250, 252sseldd 3927 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 𝑥𝐴 𝐵)
254 elinel2 4135 . . . . . . . . . . . . . 14 (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → 𝑏 ∈ Fin)
255254adantl 482 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ Fin)
256253, 255elind 4133 . . . . . . . . . . . 12 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
257256ad4ant24 751 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
2582573adant3 1131 . . . . . . . . . 10 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → 𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
259221ad2antrr 723 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ*)
2602593adant3 1131 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ*)
261 nfv 1921 . . . . . . . . . . . . . . . 16 𝑘((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin))
262226adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑥𝑦 𝐵 ∈ V)
263230adantlr 712 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
264243adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) ∈ ℝ)
265251elpwid 4550 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → 𝑏 𝑥𝑦 𝐵)
266265adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 𝑥𝑦 𝐵)
267261, 262, 263, 264, 266sge0ssrempt 43914 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ)
268267rexrd 11026 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ*)
269268adantlr 712 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ*)
270 rpxr 12738 . . . . . . . . . . . . . 14 (𝑝 ∈ ℝ+𝑝 ∈ ℝ*)
271270ad2antlr 724 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ*)
272269, 271xaddcld 13034 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) ∈ ℝ*)
2732723adant3 1131 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) ∈ ℝ*)
274 simp3 1137 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
275241, 214eqtr2d 2781 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)))
276275adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)))
2772763ad2ant1 1132 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)))
278267adantlr 712 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ)
279 rpre 12737 . . . . . . . . . . . . . . . 16 (𝑝 ∈ ℝ+𝑝 ∈ ℝ)
280279ad2antlr 724 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ)
281 rexadd 12965 . . . . . . . . . . . . . . 15 (((Σ^‘(𝑘𝑏𝐶)) ∈ ℝ ∧ 𝑝 ∈ ℝ) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) = ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
282278, 280, 281syl2anc 584 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) = ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
2832823adant3 1131 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) = ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
284277, 283breq12d 5092 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → (Σ𝑥𝑦^‘(𝑘𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) ↔ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)))
285274, 284mpbird 256 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
286260, 273, 285xrltled 12883 . . . . . . . . . 10 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
287 rspe 3235 . . . . . . . . . 10 ((𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) ∧ Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝)) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
288258, 286, 287syl2anc 584 . . . . . . . . 9 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
2892883exp 1118 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))))
290246, 247, 289rexlimd 3248 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → (∃𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)(Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝)))
291245, 290mpd 15 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
292216, 217, 219, 221, 291sge0gerpmpt 43911 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
293215, 292eqbrtrd 5101 . . . 4 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
294293ralrimiva 3110 . . 3 (𝜑 → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
295 eqid 2740 . . . . 5 (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))
296179, 295fmptd 6985 . . . 4 (𝜑 → (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))):𝐴⟶(0[,]+∞))
297132, 296, 1sge0lefi 43907 . . 3 (𝜑 → ((Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ↔ ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶))))
298294, 297mpbird 256 . 2 (𝜑 → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
2991, 2, 192, 298xrletrid 12888 1 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1086   = wceq 1542  wcel 2110  wne 2945  wral 3066  wrex 3067  {crab 3070  Vcvv 3431  csb 3837  cin 3891  wss 3892  c0 4262  𝒫 cpw 4539   ciun 4930  Disj wdisj 5044   class class class wbr 5079  cmpt 5162  cres 5592  wf 6428  cfv 6432  (class class class)co 7271  Fincfn 8716  cc 10870  cr 10871  0cc0 10872   + caddc 10875  +∞cpnf 11007  *cxr 11009   < clt 11010  cle 11011  +crp 12729   +𝑒 cxad 12845  [,)cico 13080  [,]cicc 13081  Σcsu 15395  Σ^csumge0 43871
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582  ax-inf2 9377  ax-ac2 10220  ax-cnex 10928  ax-resscn 10929  ax-1cn 10930  ax-icn 10931  ax-addcl 10932  ax-addrcl 10933  ax-mulcl 10934  ax-mulrcl 10935  ax-mulcom 10936  ax-addass 10937  ax-mulass 10938  ax-distr 10939  ax-i2m1 10940  ax-1ne0 10941  ax-1rid 10942  ax-rnegex 10943  ax-rrecex 10944  ax-cnre 10945  ax-pre-lttri 10946  ax-pre-lttrn 10947  ax-pre-ltadd 10948  ax-pre-mulgt0 10949  ax-pre-sup 10950
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-int 4886  df-iun 4932  df-disj 5045  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6201  df-ord 6268  df-on 6269  df-lim 6270  df-suc 6271  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-isom 6441  df-riota 7228  df-ov 7274  df-oprab 7275  df-mpo 7276  df-om 7707  df-1st 7824  df-2nd 7825  df-frecs 8088  df-wrecs 8119  df-recs 8193  df-rdg 8232  df-1o 8288  df-er 8481  df-map 8600  df-en 8717  df-dom 8718  df-sdom 8719  df-fin 8720  df-sup 9179  df-oi 9247  df-card 9698  df-acn 9701  df-ac 9873  df-pnf 11012  df-mnf 11013  df-xr 11014  df-ltxr 11015  df-le 11016  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-n0 12234  df-z 12320  df-uz 12582  df-rp 12730  df-xadd 12848  df-ico 13084  df-icc 13085  df-fz 13239  df-fzo 13382  df-seq 13720  df-exp 13781  df-hash 14043  df-cj 14808  df-re 14809  df-im 14810  df-sqrt 14944  df-abs 14945  df-clim 15195  df-sum 15396  df-sumge0 43872
This theorem is referenced by:  sge0iunmpt  43927
  Copyright terms: Public domain W3C validator