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 ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) )