Metamath Proof Explorer

Theorem sge0iunmptlemre

Description: Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0iunmptlemre.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
sge0iunmptlemre.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
sge0iunmptlemre.dj ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
sge0iunmptlemre.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
sge0iunmptlemre.re ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
sge0iunmptlemre.sxr ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) ∈ ℝ* )
sge0iunmptlemre.ssxr ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ∈ ℝ* )
sge0iunmptlemre.f ⊢ ( 𝜑 → ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ ( 0 [,] +∞ ) )
sge0iunmptlemre.iue ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
Assertion sge0iunmptlemre ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sge0iunmptlemre.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 sge0iunmptlemre.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
3 sge0iunmptlemre.dj ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
4 sge0iunmptlemre.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
5 sge0iunmptlemre.re ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
6 sge0iunmptlemre.sxr ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) ∈ ℝ* )
7 sge0iunmptlemre.ssxr ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ∈ ℝ* )
8 sge0iunmptlemre.f ⊢ ( 𝜑 → ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ ( 0 [,] +∞ ) )
9 sge0iunmptlemre.iue ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
10 elpwinss ⊢ ( 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
11 10 resmptd ⊢ ( 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) → ( ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ↾ 𝑦 ) = ( 𝑘 ∈ 𝑦 ↦ 𝐶 ) )
12 11 fveq2d ⊢ ( 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) → ( Σ^ ‘ ( ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ↾ 𝑦 ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ 𝐶 ) ) )
13 12 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ↾ 𝑦 ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ 𝐶 ) ) )
14 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) → 𝑦 ∈ Fin )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → 𝑦 ∈ Fin )
16 10 sselda ⊢ ( ( 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
17 eliun ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 )
18 16 17 sylib ⊢ ( ( 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ∧ 𝑘 ∈ 𝑦 ) → ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 )
19 18 adantll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 )
20 nfv ⊢ Ⅎ 𝑥 𝜑
21 nfcv ⊢ Ⅎ 𝑥 𝑦
22 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵
23 22 nfpw ⊢ Ⅎ 𝑥 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵
24 nfcv ⊢ Ⅎ 𝑥 Fin
25 23 24 nfin ⊢ Ⅎ 𝑥 ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin )
26 21 25 nfel ⊢ Ⅎ 𝑥 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin )
27 20 26 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) )
28 nfv ⊢ Ⅎ 𝑥 𝑘 ∈ 𝑦
29 27 28 nfan ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 )
30 nfv ⊢ Ⅎ 𝑥 𝐶 ∈ ( 0 [,) +∞ )
31 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝐵 )
32 eqid ⊢ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐵 ↦ 𝐶 )
33 32 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝐵 ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
34 31 4 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
35 34 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 = ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) )
36 4 3expa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
37 36 32 fmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
38 37 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
39 2 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐵 ∈ 𝑊 )
40 5 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
41 39 38 40 sge0rern ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → ¬ +∞ ∈ ran ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) )
42 38 41 fge0iccico ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( 0 [,) +∞ ) )
43 42 31 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) ∈ ( 0 [,) +∞ ) )
44 35 43 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,) +∞ ) )
45 44 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,) +∞ ) ) ) )
46 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,) +∞ ) ) ) )
47 29 30 46 rexlimd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → ( ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,) +∞ ) ) )
48 19 47 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝐶 ∈ ( 0 [,) +∞ ) )
49 15 48 sge0fsummpt ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ 𝐶 ) ) = Σ 𝑘 ∈ 𝑦 𝐶 )
50 sseqin2 ⊢ ( 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦 ) = 𝑦 )
51 50 biimpi ⊢ ( 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦 ) = 𝑦 )
52 51 eqcomd ⊢ ( 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦 ) )
53 iunin1 ⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝑦 ) = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦 )
54 53 a1i ⊢ ( 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝑦 ) = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦 ) )
55 52 54 eqtr4d ⊢ ( 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 = ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝑦 ) )
56 10 55 syl ⊢ ( 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) → 𝑦 = ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝑦 ) )
57 56 sumeq1d ⊢ ( 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) → Σ 𝑘 ∈ 𝑦 𝐶 = Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝑦 ) 𝐶 )
58 57 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑦 𝐶 = Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝑦 ) 𝐶 )
59 simpl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → 𝜑 )
60 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ Fin ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
61 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ Fin ) → Disj 𝑥 ∈ 𝐴 𝐵 )
62 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
63 ax-resscn ⊢ ℝ ⊆ ℂ
64 62 63 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
65 64 44 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
66 65 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ Fin ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
67 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ Fin ) → 𝑦 ∈ Fin )
68 60 61 66 67 fsumiunss ⊢ ( ( 𝜑 ∧ 𝑦 ∈ Fin ) → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝑦 ) 𝐶 = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶 )
69 59 15 68 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝑦 ) 𝐶 = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶 )
70 58 69 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑦 𝐶 = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶 )
71 13 49 70 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ↾ 𝑦 ) ) = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶 )
72 60 61 67 disjinfi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ Fin ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ∈ Fin )
73 id ⊢ ( 𝑦 ∈ Fin → 𝑦 ∈ Fin )
74 inss2 ⊢ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ⊆ 𝑦
75 74 a1i ⊢ ( 𝑦 ∈ Fin → ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ⊆ 𝑦 )
76 ssfi ⊢ ( ( 𝑦 ∈ Fin ∧ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ⊆ 𝑦 ) → ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ∈ Fin )
77 73 75 76 syl2anc ⊢ ( 𝑦 ∈ Fin → ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ∈ Fin )
78 77 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ Fin ) ∧ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) → ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ∈ Fin )
79 simpll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) ∧ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ) → 𝜑 )
80 elrabi ⊢ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } → 𝑤 ∈ 𝐴 )
81 80 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) ∧ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ) → 𝑤 ∈ 𝐴 )
82 elinel1 ⊢ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) → 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
83 82 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) ∧ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ) → 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
84 nfv ⊢ Ⅎ 𝑥 𝑤 ∈ 𝐴
85 nfcv ⊢ Ⅎ 𝑥 𝑘
86 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝐵
87 85 86 nfel ⊢ Ⅎ 𝑥 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵
88 20 84 87 nf3an ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
89 88 30 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) → 𝐶 ∈ ( 0 [,) +∞ ) )
90 eleq1w ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
91 csbeq1a ⊢ ( 𝑥 = 𝑤 → 𝐵 = ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
92 91 eleq2d ⊢ ( 𝑥 = 𝑤 → ( 𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) )
93 90 92 3anbi23d ⊢ ( 𝑥 = 𝑤 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ↔ ( 𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) ) )
94 93 imbi1d ⊢ ( 𝑥 = 𝑤 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,) +∞ ) ) ↔ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) → 𝐶 ∈ ( 0 [,) +∞ ) ) ) )
95 89 94 44 chvarfv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) → 𝐶 ∈ ( 0 [,) +∞ ) )
96 79 81 83 95 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) ∧ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ) → 𝐶 ∈ ( 0 [,) +∞ ) )
97 96 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ Fin ) ∧ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) ∧ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ) → 𝐶 ∈ ( 0 [,) +∞ ) )
98 78 97 fsumge0cl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ Fin ) ∧ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) → Σ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) 𝐶 ∈ ( 0 [,) +∞ ) )
99 72 98 sge0fsummpt ⊢ ( ( 𝜑 ∧ 𝑦 ∈ Fin ) → ( Σ^ ‘ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ Σ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) 𝐶 ) ) = Σ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } Σ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) 𝐶 )
100 inss2 ⊢ ( 𝐵 ∩ 𝑦 ) ⊆ 𝑦
101 100 a1i ⊢ ( 𝑦 ∈ Fin → ( 𝐵 ∩ 𝑦 ) ⊆ 𝑦 )
102 ssfi ⊢ ( ( 𝑦 ∈ Fin ∧ ( 𝐵 ∩ 𝑦 ) ⊆ 𝑦 ) → ( 𝐵 ∩ 𝑦 ) ∈ Fin )
103 73 101 102 syl2anc ⊢ ( 𝑦 ∈ Fin → ( 𝐵 ∩ 𝑦 ) ∈ Fin )
104 103 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) → ( 𝐵 ∩ 𝑦 ) ∈ Fin )
105 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) ∧ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ) → 𝜑 )
106 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐵 ∩ 𝑦 ) ≠ ∅ ) )
107 106 biimpi ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } → ( 𝑥 ∈ 𝐴 ∧ ( 𝐵 ∩ 𝑦 ) ≠ ∅ ) )
108 107 simpld ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } → 𝑥 ∈ 𝐴 )
109 108 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) ∧ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ) → 𝑥 ∈ 𝐴 )
110 elinel1 ⊢ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) → 𝑘 ∈ 𝐵 )
111 110 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) ∧ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ) → 𝑘 ∈ 𝐵 )
112 105 109 111 44 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) ∧ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ) → 𝐶 ∈ ( 0 [,) +∞ ) )
113 112 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) ∧ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ) → 𝐶 ∈ ( 0 [,) +∞ ) )
114 104 113 sge0fsummpt ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) = Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶 )
115 114 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ Fin ) → ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) = ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶 ) )
116 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ }
117 nfcv ⊢ Ⅎ 𝑤 { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ }
118 nfcv ⊢ Ⅎ 𝑤 Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶
119 86 21 nfin ⊢ Ⅎ 𝑥 ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 )
120 nfcv ⊢ Ⅎ 𝑥 𝐶
121 119 120 nfsum ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) 𝐶
122 91 ineq1d ⊢ ( 𝑥 = 𝑤 → ( 𝐵 ∩ 𝑦 ) = ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) )
123 122 sumeq1d ⊢ ( 𝑥 = 𝑤 → Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶 = Σ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) 𝐶 )
124 116 117 118 121 123 cbvmptf ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶 ) = ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ Σ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) 𝐶 )
125 124 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ Fin ) → ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶 ) = ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ Σ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) 𝐶 ) )
126 115 125 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ Fin ) → ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ Σ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) 𝐶 ) = ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) )
127 126 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ Fin ) → ( Σ^ ‘ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ Σ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) )
128 127 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ Fin ) → ( Σ^ ‘ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ Σ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) 𝐶 ) ) )
129 123 117 116 118 121 cbvsum ⊢ Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶 = Σ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } Σ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) 𝐶
130 129 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ Fin ) → Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶 = Σ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } Σ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) 𝐶 )
131 99 128 130 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ Fin ) → ( Σ^ ‘ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶 )
132 59 15 131 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) = Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶 )
133 132 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → Σ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } Σ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) 𝐶 = ( Σ^ ‘ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) )
134 71 133 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ↾ 𝑦 ) ) = ( Σ^ ‘ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) )
135 80 ssriv ⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ⊆ 𝐴
136 135 a1i ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ⊆ 𝐴 )
137 1 136 ssexd ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ∈ V )
138 vex ⊢ 𝑦 ∈ V
139 138 inex2 ⊢ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ∈ V
140 139 a1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ∈ V )
141 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
142 simpll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ) → 𝜑 )
143 simplr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ) → 𝑤 ∈ 𝐴 )
144 82 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ) → 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
145 142 143 144 95 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ) → 𝐶 ∈ ( 0 [,) +∞ ) )
146 141 145 sselid ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
147 eqid ⊢ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) = ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 )
148 146 147 fmptd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) : ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ⟶ ( 0 [,] +∞ ) )
149 140 148 sge0cl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ∈ ( 0 [,] +∞ ) )
150 80 149 sylan2 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ) → ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ∈ ( 0 [,] +∞ ) )
151 nfcv ⊢ Ⅎ 𝑤 ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) )
152 nfcv ⊢ Ⅎ 𝑥 Σ^
153 119 120 nfmpt ⊢ Ⅎ 𝑥 ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 )
154 152 153 nffv ⊢ Ⅎ 𝑥 ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) )
155 122 mpteq1d ⊢ ( 𝑥 = 𝑤 → ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) = ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) )
156 155 fveq2d ⊢ ( 𝑥 = 𝑤 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) )
157 116 117 151 154 156 cbvmptf ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) = ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) )
158 150 157 fmptd ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) : { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ⟶ ( 0 [,] +∞ ) )
159 137 158 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) ∈ ℝ* )
160 159 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) ∈ ℝ* )
161 eqid ⊢ ( 𝑤 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) = ( 𝑤 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) )
162 149 161 fmptd ⊢ ( 𝜑 → ( 𝑤 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
163 1 162 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑤 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) ∈ ℝ* )
164 163 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑤 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) ∈ ℝ* )
165 59 7 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ∈ ℝ* )
166 157 fveq2i ⊢ ( Σ^ ‘ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) )
167 166 a1i ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) )
168 1 149 136 sge0lessmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑤 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) )
169 167 168 eqbrtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑤 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) )
170 169 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑤 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) )
171 151 154 156 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) = ( 𝑤 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) )
172 171 eqcomi ⊢ ( 𝑤 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) )
173 172 fveq2i ⊢ ( Σ^ ‘ ( 𝑤 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) )
174 173 a1i ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑤 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) )
175 138 inex2 ⊢ ( 𝐵 ∩ 𝑦 ) ∈ V
176 175 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ∩ 𝑦 ) ∈ V )
177 110 36 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
178 eqid ⊢ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) = ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 )
179 177 178 fmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) : ( 𝐵 ∩ 𝑦 ) ⟶ ( 0 [,] +∞ ) )
180 176 179 sge0cl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ∈ ( 0 [,] +∞ ) )
181 2 37 sge0cl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ( 0 [,] +∞ ) )
182 inss1 ⊢ ( 𝐵 ∩ 𝑦 ) ⊆ 𝐵
183 182 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ∩ 𝑦 ) ⊆ 𝐵 )
184 2 36 183 sge0lessmpt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
185 20 1 180 181 184 sge0lempt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
186 174 185 eqbrtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑤 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
187 186 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑤 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
188 160 164 165 170 187 xrletrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝑦 ) ≠ ∅ } ↦ ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵 ∩ 𝑦 ) ↦ 𝐶 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
189 134 188 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ↾ 𝑦 ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
190 189 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ( Σ^ ‘ ( ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ↾ 𝑦 ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
191 9 8 7 sge0lefi ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ↔ ∀ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ( Σ^ ‘ ( ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ↾ 𝑦 ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) )
192 190 191 mpbird ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
193 elpwinss ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 )
194 193 resmptd ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ↾ 𝑦 ) = ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
195 194 fveq2d ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ↾ 𝑦 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
196 195 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ↾ 𝑦 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
197 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ∈ Fin )
198 197 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ∈ Fin )
199 0xr ⊢ 0 ∈ ℝ*
200 199 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 0 ∈ ℝ* )
201 pnfxr ⊢ +∞ ∈ ℝ*
202 201 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → +∞ ∈ ℝ* )
203 simpll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝜑 )
204 193 sselda ⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝐴 )
205 204 adantll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝐴 )
206 203 205 2 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝐵 ∈ 𝑊 )
207 203 205 37 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
208 206 207 sge0xrcl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ* )
209 206 207 sge0ge0 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 0 ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
210 203 205 5 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
211 ltpnf ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) < +∞ )
212 210 211 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) < +∞ )
213 200 202 208 209 212 elicod ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ( 0 [,) +∞ ) )
214 198 213 sge0fsummpt ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
215 196 214 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ↾ 𝑦 ) ) = Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
216 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) )
217 9 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
218 8 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
219 218 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
220 198 210 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
221 220 rexrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ* )
222 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ )
223 iunss1 ⊢ ( 𝑦 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
224 193 223 syl ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
225 224 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
226 217 225 ssexd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V )
227 226 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V )
228 simpll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ) → 𝜑 )
229 225 sselda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ) → 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
230 228 229 218 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
231 230 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
232 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) → 𝑝 ∈ ℝ+ )
233 193 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ⊆ 𝐴 )
234 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Disj 𝑥 ∈ 𝐴 𝐵 )
235 disjss1 ⊢ ( 𝑦 ⊆ 𝐴 → ( Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑥 ∈ 𝑦 𝐵 ) )
236 233 234 235 sylc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Disj 𝑥 ∈ 𝑦 𝐵 )
237 203 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵 ) → 𝜑 )
238 205 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
239 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝐵 )
240 237 238 239 4 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
241 198 206 236 240 210 sge0iunmptlemfi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
242 214 220 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ∈ ℝ )
243 241 242 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
244 243 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
245 222 227 231 232 244 sge0ltfirpmpt ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) → ∃ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) )
246 nfv ⊢ Ⅎ 𝑏 ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ )
247 nfre1 ⊢ Ⅎ 𝑏 ∃ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≤ ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 )
248 223 sspwd ⊢ ( 𝑦 ⊆ 𝐴 → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 )
249 193 248 syl ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 )
250 249 adantr ⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 )
251 elinel1 ⊢ ( 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 )
252 251 adantl ⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 )
253 250 252 sseldd ⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 )
254 elinel2 ⊢ ( 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) → 𝑏 ∈ Fin )
255 254 adantl ⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → 𝑏 ∈ Fin )
256 253 255 elind ⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) )
257 256 ad4ant24 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) )
258 257 3adant3 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) ) → 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) )
259 221 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ* )
260 259 3adant3 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) ) → Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ* )
261 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) )
262 226 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V )
263 230 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
264 243 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
265 251 elpwid ⊢ ( 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) → 𝑏 ⊆ ∪ 𝑥 ∈ 𝑦 𝐵 )
266 265 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → 𝑏 ⊆ ∪ 𝑥 ∈ 𝑦 𝐵 )
267 261 262 263 264 266 sge0ssrempt ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) ∈ ℝ )
268 267 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) ∈ ℝ* )
269 268 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) ∈ ℝ* )
270 rpxr ⊢ ( 𝑝 ∈ ℝ+ → 𝑝 ∈ ℝ* )
271 270 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → 𝑝 ∈ ℝ* )
272 269 271 xaddcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 ) ∈ ℝ* )
273 272 3adant3 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 ) ∈ ℝ* )
274 simp3 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) )
275 241 214 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) )
276 275 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) → Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) )
277 276 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) ) → Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) )
278 267 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) ∈ ℝ )
279 rpre ⊢ ( 𝑝 ∈ ℝ+ → 𝑝 ∈ ℝ )
280 279 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → 𝑝 ∈ ℝ )
281 rexadd ⊢ ( ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) ∈ ℝ ∧ 𝑝 ∈ ℝ ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) )
282 278 280 281 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) )
283 282 3adant3 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 ) = ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) )
284 277 283 breq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) ) → ( Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 ) ↔ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) ) )
285 274 284 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) ) → Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 ) )
286 260 273 285 xrltled ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) ) → Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≤ ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 ) )
287 rspe ⊢ ( ( 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) ∧ Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≤ ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≤ ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 ) )
288 258 286 287 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) ∧ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≤ ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 ) )
289 288 3exp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) → ( 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) → ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) → ∃ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≤ ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 ) ) ) )
290 246 247 289 rexlimd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) → ( ∃ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) < ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) + 𝑝 ) → ∃ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≤ ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 ) ) )
291 245 290 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑝 ∈ ℝ+ ) → ∃ 𝑏 ∈ ( 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin ) Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≤ ( ( Σ^ ‘ ( 𝑘 ∈ 𝑏 ↦ 𝐶 ) ) +𝑒 𝑝 ) )
292 216 217 219 221 291 sge0gerpmpt ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑥 ∈ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) )
293 215 292 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ↾ 𝑦 ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) )
294 293 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ↾ 𝑦 ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) )
295 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
296 181 295 fmptd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
297 1 296 6 sge0lefi ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) ↔ ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ↾ 𝑦 ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) ) )
298 294 297 mpbird ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) )
299 6 7 192 298 xrletrid ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )