Metamath Proof Explorer


Theorem sge0f1o

Description: Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0f1o.1 𝑘 𝜑
sge0f1o.2 𝑛 𝜑
sge0f1o.3 ( 𝑘 = 𝐺𝐵 = 𝐷 )
sge0f1o.4 ( 𝜑𝐶𝑉 )
sge0f1o.5 ( 𝜑𝐹 : 𝐶1-1-onto𝐴 )
sge0f1o.6 ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) = 𝐺 )
sge0f1o.7 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
Assertion sge0f1o ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = ( Σ^ ‘ ( 𝑛𝐶𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 sge0f1o.1 𝑘 𝜑
2 sge0f1o.2 𝑛 𝜑
3 sge0f1o.3 ( 𝑘 = 𝐺𝐵 = 𝐷 )
4 sge0f1o.4 ( 𝜑𝐶𝑉 )
5 sge0f1o.5 ( 𝜑𝐹 : 𝐶1-1-onto𝐴 )
6 sge0f1o.6 ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) = 𝐺 )
7 sge0f1o.7 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
8 f1ofo ( 𝐹 : 𝐶1-1-onto𝐴𝐹 : 𝐶onto𝐴 )
9 5 8 syl ( 𝜑𝐹 : 𝐶onto𝐴 )
10 focdmex ( 𝐶𝑉 → ( 𝐹 : 𝐶onto𝐴𝐴 ∈ V ) )
11 4 9 10 sylc ( 𝜑𝐴 ∈ V )
12 11 adantr ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → 𝐴 ∈ V )
13 1 7 fmptd2f ( 𝜑 → ( 𝑘𝐴𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
14 13 adantr ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → ( 𝑘𝐴𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
15 nfv 𝑛 +∞ ∈ ran ( 𝑘𝐴𝐵 )
16 simp3 ( ( 𝜑𝑛𝐶 ∧ +∞ = 𝐷 ) → +∞ = 𝐷 )
17 f1of ( 𝐹 : 𝐶1-1-onto𝐴𝐹 : 𝐶𝐴 )
18 5 17 syl ( 𝜑𝐹 : 𝐶𝐴 )
19 18 ffvelcdmda ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) ∈ 𝐴 )
20 nfv 𝑘 ( 𝐹𝑛 ) = 𝐺
21 nfcsb1v 𝑘 ( 𝐹𝑛 ) / 𝑘 𝐵
22 21 nfeq1 𝑘 ( 𝐹𝑛 ) / 𝑘 𝐵 = 𝐷
23 20 22 nfim 𝑘 ( ( 𝐹𝑛 ) = 𝐺 ( 𝐹𝑛 ) / 𝑘 𝐵 = 𝐷 )
24 eqeq1 ( 𝑘 = ( 𝐹𝑛 ) → ( 𝑘 = 𝐺 ↔ ( 𝐹𝑛 ) = 𝐺 ) )
25 csbeq1a ( 𝑘 = ( 𝐹𝑛 ) → 𝐵 = ( 𝐹𝑛 ) / 𝑘 𝐵 )
26 25 eqeq1d ( 𝑘 = ( 𝐹𝑛 ) → ( 𝐵 = 𝐷 ( 𝐹𝑛 ) / 𝑘 𝐵 = 𝐷 ) )
27 24 26 imbi12d ( 𝑘 = ( 𝐹𝑛 ) → ( ( 𝑘 = 𝐺𝐵 = 𝐷 ) ↔ ( ( 𝐹𝑛 ) = 𝐺 ( 𝐹𝑛 ) / 𝑘 𝐵 = 𝐷 ) ) )
28 23 27 3 vtoclg1f ( ( 𝐹𝑛 ) ∈ 𝐴 → ( ( 𝐹𝑛 ) = 𝐺 ( 𝐹𝑛 ) / 𝑘 𝐵 = 𝐷 ) )
29 19 6 28 sylc ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) / 𝑘 𝐵 = 𝐷 )
30 29 eqcomd ( ( 𝜑𝑛𝐶 ) → 𝐷 = ( 𝐹𝑛 ) / 𝑘 𝐵 )
31 30 3adant3 ( ( 𝜑𝑛𝐶 ∧ +∞ = 𝐷 ) → 𝐷 = ( 𝐹𝑛 ) / 𝑘 𝐵 )
32 16 31 eqtrd ( ( 𝜑𝑛𝐶 ∧ +∞ = 𝐷 ) → +∞ = ( 𝐹𝑛 ) / 𝑘 𝐵 )
33 simpl ( ( 𝜑𝑛𝐶 ) → 𝜑 )
34 33 19 jca ( ( 𝜑𝑛𝐶 ) → ( 𝜑 ∧ ( 𝐹𝑛 ) ∈ 𝐴 ) )
35 nfv 𝑘 ( 𝐹𝑛 ) ∈ 𝐴
36 1 35 nfan 𝑘 ( 𝜑 ∧ ( 𝐹𝑛 ) ∈ 𝐴 )
37 21 nfel1 𝑘 ( 𝐹𝑛 ) / 𝑘 𝐵 ∈ ( 0 [,] +∞ )
38 36 37 nfim 𝑘 ( ( 𝜑 ∧ ( 𝐹𝑛 ) ∈ 𝐴 ) → ( 𝐹𝑛 ) / 𝑘 𝐵 ∈ ( 0 [,] +∞ ) )
39 eleq1 ( 𝑘 = ( 𝐹𝑛 ) → ( 𝑘𝐴 ↔ ( 𝐹𝑛 ) ∈ 𝐴 ) )
40 39 anbi2d ( 𝑘 = ( 𝐹𝑛 ) → ( ( 𝜑𝑘𝐴 ) ↔ ( 𝜑 ∧ ( 𝐹𝑛 ) ∈ 𝐴 ) ) )
41 25 eleq1d ( 𝑘 = ( 𝐹𝑛 ) → ( 𝐵 ∈ ( 0 [,] +∞ ) ↔ ( 𝐹𝑛 ) / 𝑘 𝐵 ∈ ( 0 [,] +∞ ) ) )
42 40 41 imbi12d ( 𝑘 = ( 𝐹𝑛 ) → ( ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) ) ↔ ( ( 𝜑 ∧ ( 𝐹𝑛 ) ∈ 𝐴 ) → ( 𝐹𝑛 ) / 𝑘 𝐵 ∈ ( 0 [,] +∞ ) ) ) )
43 38 42 7 vtoclg1f ( ( 𝐹𝑛 ) ∈ 𝐴 → ( ( 𝜑 ∧ ( 𝐹𝑛 ) ∈ 𝐴 ) → ( 𝐹𝑛 ) / 𝑘 𝐵 ∈ ( 0 [,] +∞ ) ) )
44 19 34 43 sylc ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) / 𝑘 𝐵 ∈ ( 0 [,] +∞ ) )
45 eqid ( 𝑘𝐴𝐵 ) = ( 𝑘𝐴𝐵 )
46 21 45 25 elrnmpt1sf ( ( ( 𝐹𝑛 ) ∈ 𝐴 ( 𝐹𝑛 ) / 𝑘 𝐵 ∈ ( 0 [,] +∞ ) ) → ( 𝐹𝑛 ) / 𝑘 𝐵 ∈ ran ( 𝑘𝐴𝐵 ) )
47 19 44 46 syl2anc ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) / 𝑘 𝐵 ∈ ran ( 𝑘𝐴𝐵 ) )
48 47 3adant3 ( ( 𝜑𝑛𝐶 ∧ +∞ = 𝐷 ) → ( 𝐹𝑛 ) / 𝑘 𝐵 ∈ ran ( 𝑘𝐴𝐵 ) )
49 32 48 eqeltrd ( ( 𝜑𝑛𝐶 ∧ +∞ = 𝐷 ) → +∞ ∈ ran ( 𝑘𝐴𝐵 ) )
50 49 3exp ( 𝜑 → ( 𝑛𝐶 → ( +∞ = 𝐷 → +∞ ∈ ran ( 𝑘𝐴𝐵 ) ) ) )
51 2 15 50 rexlimd ( 𝜑 → ( ∃ 𝑛𝐶 +∞ = 𝐷 → +∞ ∈ ran ( 𝑘𝐴𝐵 ) ) )
52 pnfex +∞ ∈ V
53 eqid ( 𝑛𝐶𝐷 ) = ( 𝑛𝐶𝐷 )
54 53 elrnmpt ( +∞ ∈ V → ( +∞ ∈ ran ( 𝑛𝐶𝐷 ) ↔ ∃ 𝑛𝐶 +∞ = 𝐷 ) )
55 52 54 ax-mp ( +∞ ∈ ran ( 𝑛𝐶𝐷 ) ↔ ∃ 𝑛𝐶 +∞ = 𝐷 )
56 55 biimpi ( +∞ ∈ ran ( 𝑛𝐶𝐷 ) → ∃ 𝑛𝐶 +∞ = 𝐷 )
57 51 56 impel ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → +∞ ∈ ran ( 𝑘𝐴𝐵 ) )
58 12 14 57 sge0pnfval ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = +∞ )
59 4 adantr ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → 𝐶𝑉 )
60 30 44 eqeltrd ( ( 𝜑𝑛𝐶 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
61 2 60 fmptd2f ( 𝜑 → ( 𝑛𝐶𝐷 ) : 𝐶 ⟶ ( 0 [,] +∞ ) )
62 61 adantr ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → ( 𝑛𝐶𝐷 ) : 𝐶 ⟶ ( 0 [,] +∞ ) )
63 simpr ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → +∞ ∈ ran ( 𝑛𝐶𝐷 ) )
64 59 62 63 sge0pnfval ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → ( Σ^ ‘ ( 𝑛𝐶𝐷 ) ) = +∞ )
65 58 64 eqtr4d ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = ( Σ^ ‘ ( 𝑛𝐶𝐷 ) ) )
66 sumex Σ 𝑘𝑦 𝐵 ∈ V
67 66 a1i ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘𝑦 𝐵 ∈ V )
68 cnvimass ( 𝐹𝑦 ) ⊆ dom 𝐹
69 68 18 fssdm ( 𝜑 → ( 𝐹𝑦 ) ⊆ 𝐶 )
70 4 69 sselpwd ( 𝜑 → ( 𝐹𝑦 ) ∈ 𝒫 𝐶 )
71 70 adantr ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑦 ) ∈ 𝒫 𝐶 )
72 f1ocnv ( 𝐹 : 𝐶1-1-onto𝐴 𝐹 : 𝐴1-1-onto𝐶 )
73 5 72 syl ( 𝜑 𝐹 : 𝐴1-1-onto𝐶 )
74 f1ofun ( 𝐹 : 𝐴1-1-onto𝐶 → Fun 𝐹 )
75 73 74 syl ( 𝜑 → Fun 𝐹 )
76 elinel2 ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ∈ Fin )
77 imafi ( ( Fun 𝐹𝑦 ∈ Fin ) → ( 𝐹𝑦 ) ∈ Fin )
78 75 76 77 syl2an ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑦 ) ∈ Fin )
79 71 78 elind ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) )
80 79 adantlr ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) )
81 nfv 𝑘 ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 )
82 1 81 nfan 𝑘 ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) )
83 nfv 𝑘 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin )
84 82 83 nfan 𝑘 ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) )
85 nfmpt1 𝑛 ( 𝑛𝐶𝐷 )
86 85 nfrn 𝑛 ran ( 𝑛𝐶𝐷 )
87 86 nfel2 𝑛 +∞ ∈ ran ( 𝑛𝐶𝐷 )
88 87 nfn 𝑛 ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 )
89 2 88 nfan 𝑛 ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) )
90 nfv 𝑛 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin )
91 89 90 nfan 𝑛 ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) )
92 78 adantlr ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑦 ) ∈ Fin )
93 f1of1 ( 𝐹 : 𝐶1-1-onto𝐴𝐹 : 𝐶1-1𝐴 )
94 5 93 syl ( 𝜑𝐹 : 𝐶1-1𝐴 )
95 94 adantr ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐹 : 𝐶1-1𝐴 )
96 69 adantr ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑦 ) ⊆ 𝐶 )
97 f1ores ( ( 𝐹 : 𝐶1-1𝐴 ∧ ( 𝐹𝑦 ) ⊆ 𝐶 ) → ( 𝐹 ↾ ( 𝐹𝑦 ) ) : ( 𝐹𝑦 ) –1-1-onto→ ( 𝐹 “ ( 𝐹𝑦 ) ) )
98 95 96 97 syl2anc ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ ( 𝐹𝑦 ) ) : ( 𝐹𝑦 ) –1-1-onto→ ( 𝐹 “ ( 𝐹𝑦 ) ) )
99 elpwinss ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦𝐴 )
100 foimacnv ( ( 𝐹 : 𝐶onto𝐴𝑦𝐴 ) → ( 𝐹 “ ( 𝐹𝑦 ) ) = 𝑦 )
101 9 99 100 syl2an ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 “ ( 𝐹𝑦 ) ) = 𝑦 )
102 101 f1oeq3d ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐹 ↾ ( 𝐹𝑦 ) ) : ( 𝐹𝑦 ) –1-1-onto→ ( 𝐹 “ ( 𝐹𝑦 ) ) ↔ ( 𝐹 ↾ ( 𝐹𝑦 ) ) : ( 𝐹𝑦 ) –1-1-onto𝑦 ) )
103 98 102 mpbid ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ ( 𝐹𝑦 ) ) : ( 𝐹𝑦 ) –1-1-onto𝑦 )
104 103 adantlr ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ ( 𝐹𝑦 ) ) : ( 𝐹𝑦 ) –1-1-onto𝑦 )
105 18 4 fexd ( 𝜑𝐹 ∈ V )
106 cnvexg ( 𝐹 ∈ V → 𝐹 ∈ V )
107 105 106 syl ( 𝜑 𝐹 ∈ V )
108 107 imaexd ( 𝜑 → ( 𝐹𝑦 ) ∈ V )
109 108 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑛 ∈ ( 𝐹𝑦 ) ) → ( 𝐹𝑦 ) ∈ V )
110 simpll ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑛 ∈ ( 𝐹𝑦 ) ) → 𝜑 )
111 79 adantr ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑛 ∈ ( 𝐹𝑦 ) ) → ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) )
112 simpr ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑛 ∈ ( 𝐹𝑦 ) ) → 𝑛 ∈ ( 𝐹𝑦 ) )
113 110 111 112 jca31 ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑛 ∈ ( 𝐹𝑦 ) ) → ( ( 𝜑 ∧ ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ ( 𝐹𝑦 ) ) )
114 eleq1 ( 𝑥 = ( 𝐹𝑦 ) → ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ↔ ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) )
115 114 anbi2d ( 𝑥 = ( 𝐹𝑦 ) → ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ↔ ( 𝜑 ∧ ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ) )
116 eleq2w2 ( 𝑥 = ( 𝐹𝑦 ) → ( 𝑛𝑥𝑛 ∈ ( 𝐹𝑦 ) ) )
117 115 116 anbi12d ( 𝑥 = ( 𝐹𝑦 ) → ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛𝑥 ) ↔ ( ( 𝜑 ∧ ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ ( 𝐹𝑦 ) ) ) )
118 reseq2 ( 𝑥 = ( 𝐹𝑦 ) → ( 𝐹𝑥 ) = ( 𝐹 ↾ ( 𝐹𝑦 ) ) )
119 118 fveq1d ( 𝑥 = ( 𝐹𝑦 ) → ( ( 𝐹𝑥 ) ‘ 𝑛 ) = ( ( 𝐹 ↾ ( 𝐹𝑦 ) ) ‘ 𝑛 ) )
120 119 eqeq1d ( 𝑥 = ( 𝐹𝑦 ) → ( ( ( 𝐹𝑥 ) ‘ 𝑛 ) = 𝐺 ↔ ( ( 𝐹 ↾ ( 𝐹𝑦 ) ) ‘ 𝑛 ) = 𝐺 ) )
121 117 120 imbi12d ( 𝑥 = ( 𝐹𝑦 ) → ( ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛𝑥 ) → ( ( 𝐹𝑥 ) ‘ 𝑛 ) = 𝐺 ) ↔ ( ( ( 𝜑 ∧ ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ ( 𝐹𝑦 ) ) → ( ( 𝐹 ↾ ( 𝐹𝑦 ) ) ‘ 𝑛 ) = 𝐺 ) ) )
122 fvres ( 𝑛𝑥 → ( ( 𝐹𝑥 ) ‘ 𝑛 ) = ( 𝐹𝑛 ) )
123 122 adantl ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛𝑥 ) → ( ( 𝐹𝑥 ) ‘ 𝑛 ) = ( 𝐹𝑛 ) )
124 simpll ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛𝑥 ) → 𝜑 )
125 elpwinss ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) → 𝑥𝐶 )
126 125 adantl ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → 𝑥𝐶 )
127 126 sselda ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛𝑥 ) → 𝑛𝐶 )
128 124 127 6 syl2anc ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛𝑥 ) → ( 𝐹𝑛 ) = 𝐺 )
129 123 128 eqtrd ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛𝑥 ) → ( ( 𝐹𝑥 ) ‘ 𝑛 ) = 𝐺 )
130 121 129 vtoclg ( ( 𝐹𝑦 ) ∈ V → ( ( ( 𝜑 ∧ ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ ( 𝐹𝑦 ) ) → ( ( 𝐹 ↾ ( 𝐹𝑦 ) ) ‘ 𝑛 ) = 𝐺 ) )
131 109 113 130 sylc ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑛 ∈ ( 𝐹𝑦 ) ) → ( ( 𝐹 ↾ ( 𝐹𝑦 ) ) ‘ 𝑛 ) = 𝐺 )
132 131 adantllr ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑛 ∈ ( 𝐹𝑦 ) ) → ( ( 𝐹 ↾ ( 𝐹𝑦 ) ) ‘ 𝑛 ) = 𝐺 )
133 108 ad3antrrr ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑦 ) → ( 𝐹𝑦 ) ∈ V )
134 simpll ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑦 ) → ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) )
135 70 ad3antrrr ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑦 ) → ( 𝐹𝑦 ) ∈ 𝒫 𝐶 )
136 92 adantr ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑦 ) → ( 𝐹𝑦 ) ∈ Fin )
137 135 136 elind ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑦 ) → ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) )
138 simpr ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑦 ) → 𝑘𝑦 )
139 101 eqcomd ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 = ( 𝐹 “ ( 𝐹𝑦 ) ) )
140 139 adantr ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑦 ) → 𝑦 = ( 𝐹 “ ( 𝐹𝑦 ) ) )
141 138 140 eleqtrd ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑦 ) → 𝑘 ∈ ( 𝐹 “ ( 𝐹𝑦 ) ) )
142 141 adantllr ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑦 ) → 𝑘 ∈ ( 𝐹 “ ( 𝐹𝑦 ) ) )
143 134 137 142 jca31 ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑦 ) → ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ ( 𝐹𝑦 ) ) ) )
144 114 anbi2d ( 𝑥 = ( 𝐹𝑦 ) → ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ↔ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ) )
145 imaeq2 ( 𝑥 = ( 𝐹𝑦 ) → ( 𝐹𝑥 ) = ( 𝐹 “ ( 𝐹𝑦 ) ) )
146 145 eleq2d ( 𝑥 = ( 𝐹𝑦 ) → ( 𝑘 ∈ ( 𝐹𝑥 ) ↔ 𝑘 ∈ ( 𝐹 “ ( 𝐹𝑦 ) ) ) )
147 144 146 anbi12d ( 𝑥 = ( 𝐹𝑦 ) → ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹𝑥 ) ) ↔ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ ( 𝐹𝑦 ) ) ) ) )
148 147 imbi1d ( 𝑥 = ( 𝐹𝑦 ) → ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹𝑥 ) ) → 𝐵 ∈ ℂ ) ↔ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ ( 𝐹𝑦 ) ) ) → 𝐵 ∈ ℂ ) ) )
149 rge0ssre ( 0 [,) +∞ ) ⊆ ℝ
150 ax-resscn ℝ ⊆ ℂ
151 149 150 sstri ( 0 [,) +∞ ) ⊆ ℂ
152 simplll ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹𝑥 ) ) → 𝜑 )
153 simpllr ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹𝑥 ) ) → ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) )
154 18 fimassd ( 𝜑 → ( 𝐹𝑥 ) ⊆ 𝐴 )
155 154 ad2antrr ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹𝑥 ) ) → ( 𝐹𝑥 ) ⊆ 𝐴 )
156 simpr ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹𝑥 ) ) → 𝑘 ∈ ( 𝐹𝑥 ) )
157 155 156 sseldd ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹𝑥 ) ) → 𝑘𝐴 )
158 157 adantllr ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹𝑥 ) ) → 𝑘𝐴 )
159 foelcdmi ( ( 𝐹 : 𝐶onto𝐴𝑘𝐴 ) → ∃ 𝑛𝐶 ( 𝐹𝑛 ) = 𝑘 )
160 9 159 sylan ( ( 𝜑𝑘𝐴 ) → ∃ 𝑛𝐶 ( 𝐹𝑛 ) = 𝑘 )
161 160 adantlr ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑘𝐴 ) → ∃ 𝑛𝐶 ( 𝐹𝑛 ) = 𝑘 )
162 nfv 𝑛 𝑘𝐴
163 89 162 nfan 𝑛 ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑘𝐴 )
164 nfv 𝑛 𝐵 ∈ ( 0 [,) +∞ )
165 csbid 𝑘 / 𝑘 𝐵 = 𝐵
166 165 eqcomi 𝐵 = 𝑘 / 𝑘 𝐵
167 166 a1i ( ( 𝜑𝑛𝐶 ∧ ( 𝐹𝑛 ) = 𝑘 ) → 𝐵 = 𝑘 / 𝑘 𝐵 )
168 id ( ( 𝐹𝑛 ) = 𝑘 → ( 𝐹𝑛 ) = 𝑘 )
169 168 eqcomd ( ( 𝐹𝑛 ) = 𝑘𝑘 = ( 𝐹𝑛 ) )
170 169 csbeq1d ( ( 𝐹𝑛 ) = 𝑘 𝑘 / 𝑘 𝐵 = ( 𝐹𝑛 ) / 𝑘 𝐵 )
171 170 3ad2ant3 ( ( 𝜑𝑛𝐶 ∧ ( 𝐹𝑛 ) = 𝑘 ) → 𝑘 / 𝑘 𝐵 = ( 𝐹𝑛 ) / 𝑘 𝐵 )
172 29 3adant3 ( ( 𝜑𝑛𝐶 ∧ ( 𝐹𝑛 ) = 𝑘 ) → ( 𝐹𝑛 ) / 𝑘 𝐵 = 𝐷 )
173 167 171 172 3eqtrd ( ( 𝜑𝑛𝐶 ∧ ( 𝐹𝑛 ) = 𝑘 ) → 𝐵 = 𝐷 )
174 173 3adant1r ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑛𝐶 ∧ ( 𝐹𝑛 ) = 𝑘 ) → 𝐵 = 𝐷 )
175 0xr 0 ∈ ℝ*
176 175 a1i ( ( ( 𝜑𝑛𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → 0 ∈ ℝ* )
177 pnfxr +∞ ∈ ℝ*
178 177 a1i ( ( ( 𝜑𝑛𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → +∞ ∈ ℝ* )
179 60 adantr ( ( ( 𝜑𝑛𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → 𝐷 ∈ ( 0 [,] +∞ ) )
180 simpr ( ( ( 𝜑𝑛𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → ¬ 𝐷 ∈ ( 0 [,) +∞ ) )
181 176 178 179 180 eliccnelico ( ( ( 𝜑𝑛𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → 𝐷 = +∞ )
182 181 eqcomd ( ( ( 𝜑𝑛𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → +∞ = 𝐷 )
183 simpr ( ( 𝜑𝑛𝐶 ) → 𝑛𝐶 )
184 53 183 60 elrnmpt1d ( ( 𝜑𝑛𝐶 ) → 𝐷 ∈ ran ( 𝑛𝐶𝐷 ) )
185 184 adantr ( ( ( 𝜑𝑛𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → 𝐷 ∈ ran ( 𝑛𝐶𝐷 ) )
186 182 185 eqeltrd ( ( ( 𝜑𝑛𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → +∞ ∈ ran ( 𝑛𝐶𝐷 ) )
187 186 adantllr ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑛𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → +∞ ∈ ran ( 𝑛𝐶𝐷 ) )
188 simpllr ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑛𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) )
189 187 188 condan ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑛𝐶 ) → 𝐷 ∈ ( 0 [,) +∞ ) )
190 189 3adant3 ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑛𝐶 ∧ ( 𝐹𝑛 ) = 𝑘 ) → 𝐷 ∈ ( 0 [,) +∞ ) )
191 174 190 eqeltrd ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑛𝐶 ∧ ( 𝐹𝑛 ) = 𝑘 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
192 191 3exp ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → ( 𝑛𝐶 → ( ( 𝐹𝑛 ) = 𝑘𝐵 ∈ ( 0 [,) +∞ ) ) ) )
193 192 adantr ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑘𝐴 ) → ( 𝑛𝐶 → ( ( 𝐹𝑛 ) = 𝑘𝐵 ∈ ( 0 [,) +∞ ) ) ) )
194 163 164 193 rexlimd ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑘𝐴 ) → ( ∃ 𝑛𝐶 ( 𝐹𝑛 ) = 𝑘𝐵 ∈ ( 0 [,) +∞ ) ) )
195 161 194 mpd ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑘𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
196 152 153 158 195 syl21anc ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹𝑥 ) ) → 𝐵 ∈ ( 0 [,) +∞ ) )
197 151 196 sselid ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹𝑥 ) ) → 𝐵 ∈ ℂ )
198 148 197 vtoclg ( ( 𝐹𝑦 ) ∈ V → ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ ( 𝐹𝑦 ) ) ) → 𝐵 ∈ ℂ ) )
199 133 143 198 sylc ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑦 ) → 𝐵 ∈ ℂ )
200 84 91 3 92 104 132 199 fsumf1of ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘𝑦 𝐵 = Σ 𝑛 ∈ ( 𝐹𝑦 ) 𝐷 )
201 sumeq1 ( 𝑥 = ( 𝐹𝑦 ) → Σ 𝑛𝑥 𝐷 = Σ 𝑛 ∈ ( 𝐹𝑦 ) 𝐷 )
202 201 rspceeqv ( ( ( 𝐹𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ Σ 𝑘𝑦 𝐵 = Σ 𝑛 ∈ ( 𝐹𝑦 ) 𝐷 ) → ∃ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) Σ 𝑘𝑦 𝐵 = Σ 𝑛𝑥 𝐷 )
203 80 200 202 syl2anc ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∃ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) Σ 𝑘𝑦 𝐵 = Σ 𝑛𝑥 𝐷 )
204 67 203 rnmptssrn ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘𝑦 𝐵 ) ⊆ ran ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ Σ 𝑛𝑥 𝐷 ) )
205 sumex Σ 𝑛𝑥 𝐷 ∈ V
206 205 a1i ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → Σ 𝑛𝑥 𝐷 ∈ V )
207 11 154 sselpwd ( 𝜑 → ( 𝐹𝑥 ) ∈ 𝒫 𝐴 )
208 207 adantr ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹𝑥 ) ∈ 𝒫 𝐴 )
209 18 ffund ( 𝜑 → Fun 𝐹 )
210 elinel2 ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) → 𝑥 ∈ Fin )
211 imafi ( ( Fun 𝐹𝑥 ∈ Fin ) → ( 𝐹𝑥 ) ∈ Fin )
212 209 210 211 syl2an ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹𝑥 ) ∈ Fin )
213 208 212 elind ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹𝑥 ) ∈ ( 𝒫 𝐴 ∩ Fin ) )
214 213 adantlr ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹𝑥 ) ∈ ( 𝒫 𝐴 ∩ Fin ) )
215 nfv 𝑘 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin )
216 82 215 nfan 𝑘 ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) )
217 nfv 𝑛 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin )
218 89 217 nfan 𝑛 ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) )
219 210 adantl ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → 𝑥 ∈ Fin )
220 f1ores ( ( 𝐹 : 𝐶1-1𝐴𝑥𝐶 ) → ( 𝐹𝑥 ) : 𝑥1-1-onto→ ( 𝐹𝑥 ) )
221 94 125 220 syl2an ( ( 𝜑𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹𝑥 ) : 𝑥1-1-onto→ ( 𝐹𝑥 ) )
222 221 adantlr ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹𝑥 ) : 𝑥1-1-onto→ ( 𝐹𝑥 ) )
223 129 adantllr ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛𝑥 ) → ( ( 𝐹𝑥 ) ‘ 𝑛 ) = 𝐺 )
224 216 218 3 219 222 223 197 fsumf1of ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → Σ 𝑘 ∈ ( 𝐹𝑥 ) 𝐵 = Σ 𝑛𝑥 𝐷 )
225 224 eqcomd ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → Σ 𝑛𝑥 𝐷 = Σ 𝑘 ∈ ( 𝐹𝑥 ) 𝐵 )
226 sumeq1 ( 𝑦 = ( 𝐹𝑥 ) → Σ 𝑘𝑦 𝐵 = Σ 𝑘 ∈ ( 𝐹𝑥 ) 𝐵 )
227 226 rspceeqv ( ( ( 𝐹𝑥 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ Σ 𝑛𝑥 𝐷 = Σ 𝑘 ∈ ( 𝐹𝑥 ) 𝐵 ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑛𝑥 𝐷 = Σ 𝑘𝑦 𝐵 )
228 214 225 227 syl2anc ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑛𝑥 𝐷 = Σ 𝑘𝑦 𝐵 )
229 206 228 rnmptssrn ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → ran ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ Σ 𝑛𝑥 𝐷 ) ⊆ ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘𝑦 𝐵 ) )
230 204 229 eqssd ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘𝑦 𝐵 ) = ran ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ Σ 𝑛𝑥 𝐷 ) )
231 230 supeq1d ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘𝑦 𝐵 ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ Σ 𝑛𝑥 𝐷 ) , ℝ* , < ) )
232 11 adantr ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → 𝐴 ∈ V )
233 82 232 195 sge0revalmpt ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘𝑦 𝐵 ) , ℝ* , < ) )
234 4 adantr ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → 𝐶𝑉 )
235 89 234 189 sge0revalmpt ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → ( Σ^ ‘ ( 𝑛𝐶𝐷 ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ Σ 𝑛𝑥 𝐷 ) , ℝ* , < ) )
236 231 233 235 3eqtr4d ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛𝐶𝐷 ) ) → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = ( Σ^ ‘ ( 𝑛𝐶𝐷 ) ) )
237 65 236 pm2.61dan ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = ( Σ^ ‘ ( 𝑛𝐶𝐷 ) ) )