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