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