Metamath Proof Explorer

Theorem sge0iunmpt

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

Ref Expression
Hypotheses sge0iunmpt.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
sge0iunmpt.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
sge0iunmpt.dj ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
sge0iunmpt.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
Assertion sge0iunmpt ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sge0iunmpt.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 sge0iunmpt.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
3 sge0iunmpt.dj ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
4 sge0iunmpt.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
5 nfv ⊢ Ⅎ 𝑥 𝜑
6 nfcv ⊢ Ⅎ 𝑥 Σ^
7 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵
8 nfcv ⊢ Ⅎ 𝑥 𝐶
9 7 8 nfmpt ⊢ Ⅎ 𝑥 ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 )
10 6 9 nffv ⊢ Ⅎ 𝑥 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) )
11 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
12 6 11 nffv ⊢ Ⅎ 𝑥 ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
13 10 12 nfeq ⊢ Ⅎ 𝑥 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
14 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 )
15 iunexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
16 1 14 15 syl2anc ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
17 eliun ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 )
18 17 biimpi ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 )
20 nfcv ⊢ Ⅎ 𝑥 𝑘
21 20 7 nfel ⊢ Ⅎ 𝑥 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
22 5 21 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
23 8 nfel1 ⊢ Ⅎ 𝑥 𝐶 ∈ ( 0 [,] +∞ )
24 4 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) ) )
26 22 23 25 rexlimd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) )
27 19 26 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
28 eqid ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 )
29 27 28 fmptd ⊢ ( 𝜑 → ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ ( 0 [,] +∞ ) )
30 16 29 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) ∈ ℝ* )
31 30 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) ∈ ℝ* )
32 id ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ )
33 32 eqcomd ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ → +∞ = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
34 33 adantl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → +∞ = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
35 34 3adant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → +∞ = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
36 16 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
37 27 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
38 ssiun2 ⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
40 36 37 39 sge0lessmpt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) )
41 40 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) )
42 35 41 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → +∞ ≤ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) )
43 31 42 xrgepnfd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = +∞ )
44 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → 𝐴 ∈ 𝑉 )
45 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ 𝐴 )
46 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
47 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝑊
48 46 47 nfel ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑊
49 45 48 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑊 )
50 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
51 50 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ) )
52 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
53 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝑊 = ⦋ 𝑦 / 𝑥 ⦌ 𝑊 )
54 52 53 eleq12d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∈ 𝑊 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑊 ) )
55 51 54 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑊 ) ) )
56 49 55 2 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑊 )
57 56 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑊 )
58 46 8 nfmpt ⊢ Ⅎ 𝑥 ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ 𝐶 )
59 nfcv ⊢ Ⅎ 𝑥 ( 0 [,] +∞ )
60 58 46 59 nff ⊢ Ⅎ 𝑥 ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) : ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟶ ( 0 [,] +∞ )
61 45 60 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) : ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟶ ( 0 [,] +∞ ) )
62 52 mpteq1d ⊢ ( 𝑥 = 𝑦 → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) )
63 62 52 feq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( 0 [,] +∞ ) ↔ ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) : ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟶ ( 0 [,] +∞ ) ) )
64 51 63 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( 0 [,] +∞ ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) : ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟶ ( 0 [,] +∞ ) ) ) )
65 24 imp31 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
66 eqid ⊢ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐵 ↦ 𝐶 )
67 65 66 fmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
68 61 64 67 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) : ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟶ ( 0 [,] +∞ ) )
69 68 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) : ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟶ ( 0 [,] +∞ ) )
70 57 69 sge0cl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) ) ∈ ( 0 [,] +∞ ) )
71 nfcv ⊢ Ⅎ 𝑦 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) )
72 6 58 nffv ⊢ Ⅎ 𝑥 ( Σ^ ‘ ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) )
73 62 fveq2d ⊢ ( 𝑥 = 𝑦 → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) ) )
74 71 72 73 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) = ( 𝑦 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) ) )
75 70 74 fmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
76 75 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
77 id ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴 )
78 fvexd ⊢ ( 𝑥 ∈ 𝐴 → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ V )
79 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
80 79 elrnmpt1 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ V ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
81 77 78 80 syl2anc ⊢ ( 𝑥 ∈ 𝐴 → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
82 81 adantr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
83 34 82 eqeltrd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → +∞ ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
84 83 3adant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → +∞ ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
85 44 76 84 sge0pnfval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = +∞ )
86 43 85 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
87 86 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) ) )
88 5 13 87 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) )
89 88 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
90 simpl ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → 𝜑 )
91 ralnex ⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ↔ ¬ ∃ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ )
92 df-ne ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ↔ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ )
93 92 bicomi ⊢ ( ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ↔ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ )
94 93 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ↔ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ )
95 91 94 sylbb1 ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ → ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ )
96 95 adantl ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ )
97 1 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) → 𝐴 ∈ 𝑉 )
98 nfcv ⊢ Ⅎ 𝑥 𝑊
99 46 98 nfel ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑊
100 45 99 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑊 )
101 52 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∈ 𝑊 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑊 ) )
102 51 101 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑊 ) ) )
103 100 102 2 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑊 )
104 103 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑊 )
105 nfcv ⊢ Ⅎ 𝑦 𝐵
106 105 46 52 cbvdisj ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
107 3 106 sylib ⊢ ( 𝜑 → Disj 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
108 107 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) → Disj 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
109 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
110 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐶
111 110 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ )
112 109 111 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
113 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
114 113 3anbi3d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) )
115 csbeq1a ⊢ ( 𝑘 = 𝑗 → 𝐶 = ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
116 115 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐶 ∈ ( 0 [,] +∞ ) ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) ) )
117 114 116 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) ) ) )
118 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
119 20 46 nfel ⊢ Ⅎ 𝑥 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵
120 5 118 119 nf3an ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
121 120 23 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
122 52 eleq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
123 50 122 3anbi23d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) )
124 123 imbi1d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) ) ) )
125 121 124 4 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
126 112 117 125 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
127 126 3adant1r ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
128 simpr ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
129 simpl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ∧ 𝑦 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ )
130 simpl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) → 𝑦 ∈ 𝐴 )
131 simpr ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) → ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ )
132 nfcv ⊢ Ⅎ 𝑥 ⦋ 𝑗 / 𝑘 ⦌ 𝐶
133 46 132 nfmpt ⊢ Ⅎ 𝑥 ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
134 6 133 nffv ⊢ Ⅎ 𝑥 ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
135 nfcv ⊢ Ⅎ 𝑥 +∞
136 134 135 nfne ⊢ Ⅎ 𝑥 ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ≠ +∞
137 nfcv ⊢ Ⅎ 𝑗 𝐶
138 137 110 115 cbvmpt ⊢ ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) = ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
139 138 a1i ⊢ ( 𝑥 = 𝑦 → ( 𝑘 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) = ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
140 62 139 eqtrd ⊢ ( 𝑥 = 𝑦 → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
141 140 fveq2d ⊢ ( 𝑥 = 𝑦 → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) )
142 141 neeq1d ⊢ ( 𝑥 = 𝑦 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ↔ ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ≠ +∞ ) )
143 136 142 rspc ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ → ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ≠ +∞ ) )
144 130 131 143 sylc ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ≠ +∞ )
145 128 129 144 syl2anc ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ∧ 𝑦 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ≠ +∞ )
146 145 neneqd ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ∧ 𝑦 ∈ 𝐴 ) → ¬ ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) = +∞ )
147 146 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) ∧ 𝑦 ∈ 𝐴 ) → ¬ ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) = +∞ )
148 126 3expa ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
149 eqid ⊢ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) = ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
150 148 149 fmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) : ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟶ ( 0 [,] +∞ ) )
151 150 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) : ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟶ ( 0 [,] +∞ ) )
152 104 151 sge0repnf ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) ∧ 𝑦 ∈ 𝐴 ) → ( ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) = +∞ ) )
153 147 152 mpbird ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) ∧ 𝑦 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ∈ ℝ )
154 137 110 115 cbvmpt ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) = ( 𝑗 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
155 105 46 52 cbviun ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
156 155 mpteq1i ⊢ ( 𝑗 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) = ( 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
157 154 156 eqtri ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) = ( 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
158 157 fveq2i ⊢ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
159 158 30 eqeltrrid ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ∈ ℝ* )
160 159 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ∈ ℝ* )
161 71 134 141 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) = ( 𝑦 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) )
162 161 fveq2i ⊢ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑦 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ) )
163 2 67 sge0cl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ( 0 [,] +∞ ) )
164 163 79 fmptd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
165 1 164 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ∈ ℝ* )
166 162 165 eqeltrrid ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑦 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ) ) ∈ ℝ* )
167 166 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) → ( Σ^ ‘ ( 𝑦 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ) ) ∈ ℝ* )
168 eliun ⊢ ( 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ ∃ 𝑦 ∈ 𝐴 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
169 168 biimpi ⊢ ( 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
170 169 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → ∃ 𝑦 ∈ 𝐴 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
171 nfv ⊢ Ⅎ 𝑦 𝜑
172 nfcv ⊢ Ⅎ 𝑦 𝑗
173 nfiu1 ⊢ Ⅎ 𝑦 ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
174 172 173 nfel ⊢ Ⅎ 𝑦 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
175 171 174 nfan ⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
176 nfv ⊢ Ⅎ 𝑦 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ )
177 148 exp31 ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 → ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) ) ) )
178 177 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → ( 𝑦 ∈ 𝐴 → ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) ) ) )
179 175 176 178 rexlimd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → ( ∃ 𝑦 ∈ 𝐴 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) ) )
180 170 179 mpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
181 eqid ⊢ ( 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) = ( 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
182 180 181 fmptd ⊢ ( 𝜑 → ( 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) : ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟶ ( 0 [,] +∞ ) )
183 182 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) → ( 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) : ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟶ ( 0 [,] +∞ ) )
184 155 16 eqeltrrid ⊢ ( 𝜑 → ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ V )
185 184 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) → ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ V )
186 97 104 108 127 153 160 167 183 185 sge0iunmptlemre ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) = ( Σ^ ‘ ( 𝑦 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ) ) )
187 158 a1i ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) )
188 162 a1i ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑦 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑗 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) ) ) ) )
189 186 187 188 3eqtr4d ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ≠ +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
190 90 96 189 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑥 ∈ 𝐴 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
191 89 190 pm2.61dan ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )