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