Metamath Proof Explorer


Theorem sge0fodjrnlem

Description: Re-index a nonnegative extended sum using an onto function with disjoint range, when the empty set is assigned 0 in the sum (this is true, for example, both for measures and outer measures). (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0fodjrnlem.k 𝑘 𝜑
sge0fodjrnlem.n 𝑛 𝜑
sge0fodjrnlem.bd ( 𝑘 = 𝐺𝐵 = 𝐷 )
sge0fodjrnlem.c ( 𝜑𝐶𝑉 )
sge0fodjrnlem.f ( 𝜑𝐹 : 𝐶onto𝐴 )
sge0fodjrnlem.dj ( 𝜑Disj 𝑛𝐶 ( 𝐹𝑛 ) )
sge0fodjrnlem.fng ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) = 𝐺 )
sge0fodjrnlem.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
sge0fodjrnlem.b0 ( ( 𝜑𝑘 = ∅ ) → 𝐵 = 0 )
sge0fodjrnlem.z 𝑍 = ( 𝐹 “ { ∅ } )
Assertion sge0fodjrnlem ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = ( Σ^ ‘ ( 𝑛𝐶𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 sge0fodjrnlem.k 𝑘 𝜑
2 sge0fodjrnlem.n 𝑛 𝜑
3 sge0fodjrnlem.bd ( 𝑘 = 𝐺𝐵 = 𝐷 )
4 sge0fodjrnlem.c ( 𝜑𝐶𝑉 )
5 sge0fodjrnlem.f ( 𝜑𝐹 : 𝐶onto𝐴 )
6 sge0fodjrnlem.dj ( 𝜑Disj 𝑛𝐶 ( 𝐹𝑛 ) )
7 sge0fodjrnlem.fng ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) = 𝐺 )
8 sge0fodjrnlem.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
9 sge0fodjrnlem.b0 ( ( 𝜑𝑘 = ∅ ) → 𝐵 = 0 )
10 sge0fodjrnlem.z 𝑍 = ( 𝐹 “ { ∅ } )
11 fornex ( 𝐶𝑉 → ( 𝐹 : 𝐶onto𝐴𝐴 ∈ V ) )
12 4 5 11 sylc ( 𝜑𝐴 ∈ V )
13 difssd ( 𝜑 → ( 𝐴 ∖ { ∅ } ) ⊆ 𝐴 )
14 simpl ( ( 𝜑𝑘 ∈ ( 𝐴 ∖ { ∅ } ) ) → 𝜑 )
15 13 sselda ( ( 𝜑𝑘 ∈ ( 𝐴 ∖ { ∅ } ) ) → 𝑘𝐴 )
16 14 15 8 syl2anc ( ( 𝜑𝑘 ∈ ( 𝐴 ∖ { ∅ } ) ) → 𝐵 ∈ ( 0 [,] +∞ ) )
17 simpl ( ( 𝜑𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) ) → 𝜑 )
18 dfin4 ( 𝐴 ∩ { ∅ } ) = ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) )
19 18 eqcomi ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) = ( 𝐴 ∩ { ∅ } )
20 inss2 ( 𝐴 ∩ { ∅ } ) ⊆ { ∅ }
21 19 20 eqsstri ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) ⊆ { ∅ }
22 id ( 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) → 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) )
23 21 22 sseldi ( 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) → 𝑘 ∈ { ∅ } )
24 elsni ( 𝑘 ∈ { ∅ } → 𝑘 = ∅ )
25 23 24 syl ( 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) → 𝑘 = ∅ )
26 25 adantl ( ( 𝜑𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) ) → 𝑘 = ∅ )
27 17 26 9 syl2anc ( ( 𝜑𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) ) → 𝐵 = 0 )
28 1 12 13 16 27 sge0ss ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∖ { ∅ } ) ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) )
29 28 eqcomd ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∖ { ∅ } ) ↦ 𝐵 ) ) )
30 4 difexd ( 𝜑 → ( 𝐶𝑍 ) ∈ V )
31 eqid ( 𝑛𝐶 ↦ ( 𝐹𝑛 ) ) = ( 𝑛𝐶 ↦ ( 𝐹𝑛 ) )
32 fof ( 𝐹 : 𝐶onto𝐴𝐹 : 𝐶𝐴 )
33 5 32 syl ( 𝜑𝐹 : 𝐶𝐴 )
34 33 ffvelrnda ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) ∈ 𝐴 )
35 fveq2 ( 𝑚 = 𝑛 → ( 𝐹𝑚 ) = ( 𝐹𝑛 ) )
36 35 neeq1d ( 𝑚 = 𝑛 → ( ( 𝐹𝑚 ) ≠ ∅ ↔ ( 𝐹𝑛 ) ≠ ∅ ) )
37 36 cbvrabv { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } = { 𝑛𝐶 ∣ ( 𝐹𝑛 ) ≠ ∅ }
38 35 cbvmptv ( 𝑚𝐶 ↦ ( 𝐹𝑚 ) ) = ( 𝑛𝐶 ↦ ( 𝐹𝑛 ) )
39 38 rneqi ran ( 𝑚𝐶 ↦ ( 𝐹𝑚 ) ) = ran ( 𝑛𝐶 ↦ ( 𝐹𝑛 ) )
40 39 difeq1i ( ran ( 𝑚𝐶 ↦ ( 𝐹𝑚 ) ) ∖ { ∅ } ) = ( ran ( 𝑛𝐶 ↦ ( 𝐹𝑛 ) ) ∖ { ∅ } )
41 2 31 34 6 37 40 disjf1o ( 𝜑 → ( ( 𝑛𝐶 ↦ ( 𝐹𝑛 ) ) ↾ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ) : { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } –1-1-onto→ ( ran ( 𝑚𝐶 ↦ ( 𝐹𝑚 ) ) ∖ { ∅ } ) )
42 33 feqmptd ( 𝜑𝐹 = ( 𝑛𝐶 ↦ ( 𝐹𝑛 ) ) )
43 difssd ( 𝜑 → ( 𝐶𝑍 ) ⊆ 𝐶 )
44 43 sselda ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) → 𝑛𝐶 )
45 eldifi ( 𝑛 ∈ ( 𝐶𝑍 ) → 𝑛𝐶 )
46 45 adantr ( ( 𝑛 ∈ ( 𝐶𝑍 ) ∧ ( 𝐹𝑛 ) = ∅ ) → 𝑛𝐶 )
47 id ( ( 𝐹𝑛 ) = ∅ → ( 𝐹𝑛 ) = ∅ )
48 fvex ( 𝐹𝑛 ) ∈ V
49 48 elsn ( ( 𝐹𝑛 ) ∈ { ∅ } ↔ ( 𝐹𝑛 ) = ∅ )
50 47 49 sylibr ( ( 𝐹𝑛 ) = ∅ → ( 𝐹𝑛 ) ∈ { ∅ } )
51 50 adantl ( ( 𝑛 ∈ ( 𝐶𝑍 ) ∧ ( 𝐹𝑛 ) = ∅ ) → ( 𝐹𝑛 ) ∈ { ∅ } )
52 46 51 jca ( ( 𝑛 ∈ ( 𝐶𝑍 ) ∧ ( 𝐹𝑛 ) = ∅ ) → ( 𝑛𝐶 ∧ ( 𝐹𝑛 ) ∈ { ∅ } ) )
53 52 adantll ( ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) ∧ ( 𝐹𝑛 ) = ∅ ) → ( 𝑛𝐶 ∧ ( 𝐹𝑛 ) ∈ { ∅ } ) )
54 33 ffnd ( 𝜑𝐹 Fn 𝐶 )
55 elpreima ( 𝐹 Fn 𝐶 → ( 𝑛 ∈ ( 𝐹 “ { ∅ } ) ↔ ( 𝑛𝐶 ∧ ( 𝐹𝑛 ) ∈ { ∅ } ) ) )
56 54 55 syl ( 𝜑 → ( 𝑛 ∈ ( 𝐹 “ { ∅ } ) ↔ ( 𝑛𝐶 ∧ ( 𝐹𝑛 ) ∈ { ∅ } ) ) )
57 56 ad2antrr ( ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) ∧ ( 𝐹𝑛 ) = ∅ ) → ( 𝑛 ∈ ( 𝐹 “ { ∅ } ) ↔ ( 𝑛𝐶 ∧ ( 𝐹𝑛 ) ∈ { ∅ } ) ) )
58 53 57 mpbird ( ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) ∧ ( 𝐹𝑛 ) = ∅ ) → 𝑛 ∈ ( 𝐹 “ { ∅ } ) )
59 58 10 eleqtrrdi ( ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) ∧ ( 𝐹𝑛 ) = ∅ ) → 𝑛𝑍 )
60 eldifn ( 𝑛 ∈ ( 𝐶𝑍 ) → ¬ 𝑛𝑍 )
61 60 ad2antlr ( ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) ∧ ( 𝐹𝑛 ) = ∅ ) → ¬ 𝑛𝑍 )
62 59 61 pm2.65da ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) → ¬ ( 𝐹𝑛 ) = ∅ )
63 62 neqned ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) → ( 𝐹𝑛 ) ≠ ∅ )
64 44 63 jca ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) → ( 𝑛𝐶 ∧ ( 𝐹𝑛 ) ≠ ∅ ) )
65 36 elrab ( 𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ↔ ( 𝑛𝐶 ∧ ( 𝐹𝑛 ) ≠ ∅ ) )
66 64 65 sylibr ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) → 𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } )
67 66 ex ( 𝜑 → ( 𝑛 ∈ ( 𝐶𝑍 ) → 𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ) )
68 65 simplbi ( 𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } → 𝑛𝐶 )
69 68 adantl ( ( 𝜑𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ) → 𝑛𝐶 )
70 10 eleq2i ( 𝑛𝑍𝑛 ∈ ( 𝐹 “ { ∅ } ) )
71 70 biimpi ( 𝑛𝑍𝑛 ∈ ( 𝐹 “ { ∅ } ) )
72 71 adantl ( ( 𝜑𝑛𝑍 ) → 𝑛 ∈ ( 𝐹 “ { ∅ } ) )
73 56 adantr ( ( 𝜑𝑛𝑍 ) → ( 𝑛 ∈ ( 𝐹 “ { ∅ } ) ↔ ( 𝑛𝐶 ∧ ( 𝐹𝑛 ) ∈ { ∅ } ) ) )
74 72 73 mpbid ( ( 𝜑𝑛𝑍 ) → ( 𝑛𝐶 ∧ ( 𝐹𝑛 ) ∈ { ∅ } ) )
75 74 simprd ( ( 𝜑𝑛𝑍 ) → ( 𝐹𝑛 ) ∈ { ∅ } )
76 elsni ( ( 𝐹𝑛 ) ∈ { ∅ } → ( 𝐹𝑛 ) = ∅ )
77 75 76 syl ( ( 𝜑𝑛𝑍 ) → ( 𝐹𝑛 ) = ∅ )
78 77 adantlr ( ( ( 𝜑𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ) ∧ 𝑛𝑍 ) → ( 𝐹𝑛 ) = ∅ )
79 65 simprbi ( 𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } → ( 𝐹𝑛 ) ≠ ∅ )
80 79 ad2antlr ( ( ( 𝜑𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ) ∧ 𝑛𝑍 ) → ( 𝐹𝑛 ) ≠ ∅ )
81 80 neneqd ( ( ( 𝜑𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ) ∧ 𝑛𝑍 ) → ¬ ( 𝐹𝑛 ) = ∅ )
82 78 81 pm2.65da ( ( 𝜑𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ) → ¬ 𝑛𝑍 )
83 69 82 eldifd ( ( 𝜑𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ) → 𝑛 ∈ ( 𝐶𝑍 ) )
84 83 ex ( 𝜑 → ( 𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } → 𝑛 ∈ ( 𝐶𝑍 ) ) )
85 2 84 ralrimi ( 𝜑 → ∀ 𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } 𝑛 ∈ ( 𝐶𝑍 ) )
86 dfss3 ( { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ⊆ ( 𝐶𝑍 ) ↔ ∀ 𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } 𝑛 ∈ ( 𝐶𝑍 ) )
87 85 86 sylibr ( 𝜑 → { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ⊆ ( 𝐶𝑍 ) )
88 87 sseld ( 𝜑 → ( 𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } → 𝑛 ∈ ( 𝐶𝑍 ) ) )
89 67 88 impbid ( 𝜑 → ( 𝑛 ∈ ( 𝐶𝑍 ) ↔ 𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ) )
90 2 89 alrimi ( 𝜑 → ∀ 𝑛 ( 𝑛 ∈ ( 𝐶𝑍 ) ↔ 𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ) )
91 dfcleq ( ( 𝐶𝑍 ) = { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ↔ ∀ 𝑛 ( 𝑛 ∈ ( 𝐶𝑍 ) ↔ 𝑛 ∈ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ) )
92 90 91 sylibr ( 𝜑 → ( 𝐶𝑍 ) = { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } )
93 42 92 reseq12d ( 𝜑 → ( 𝐹 ↾ ( 𝐶𝑍 ) ) = ( ( 𝑛𝐶 ↦ ( 𝐹𝑛 ) ) ↾ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ) )
94 42 38 eqtr4di ( 𝜑𝐹 = ( 𝑚𝐶 ↦ ( 𝐹𝑚 ) ) )
95 94 eqcomd ( 𝜑 → ( 𝑚𝐶 ↦ ( 𝐹𝑚 ) ) = 𝐹 )
96 95 rneqd ( 𝜑 → ran ( 𝑚𝐶 ↦ ( 𝐹𝑚 ) ) = ran 𝐹 )
97 forn ( 𝐹 : 𝐶onto𝐴 → ran 𝐹 = 𝐴 )
98 5 97 syl ( 𝜑 → ran 𝐹 = 𝐴 )
99 96 98 eqtr2d ( 𝜑𝐴 = ran ( 𝑚𝐶 ↦ ( 𝐹𝑚 ) ) )
100 99 difeq1d ( 𝜑 → ( 𝐴 ∖ { ∅ } ) = ( ran ( 𝑚𝐶 ↦ ( 𝐹𝑚 ) ) ∖ { ∅ } ) )
101 93 92 100 f1oeq123d ( 𝜑 → ( ( 𝐹 ↾ ( 𝐶𝑍 ) ) : ( 𝐶𝑍 ) –1-1-onto→ ( 𝐴 ∖ { ∅ } ) ↔ ( ( 𝑛𝐶 ↦ ( 𝐹𝑛 ) ) ↾ { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } ) : { 𝑚𝐶 ∣ ( 𝐹𝑚 ) ≠ ∅ } –1-1-onto→ ( ran ( 𝑚𝐶 ↦ ( 𝐹𝑚 ) ) ∖ { ∅ } ) ) )
102 41 101 mpbird ( 𝜑 → ( 𝐹 ↾ ( 𝐶𝑍 ) ) : ( 𝐶𝑍 ) –1-1-onto→ ( 𝐴 ∖ { ∅ } ) )
103 fvres ( 𝑛 ∈ ( 𝐶𝑍 ) → ( ( 𝐹 ↾ ( 𝐶𝑍 ) ) ‘ 𝑛 ) = ( 𝐹𝑛 ) )
104 103 adantl ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) → ( ( 𝐹 ↾ ( 𝐶𝑍 ) ) ‘ 𝑛 ) = ( 𝐹𝑛 ) )
105 simpl ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) → 𝜑 )
106 105 44 7 syl2anc ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) → ( 𝐹𝑛 ) = 𝐺 )
107 104 106 eqtrd ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) → ( ( 𝐹 ↾ ( 𝐶𝑍 ) ) ‘ 𝑛 ) = 𝐺 )
108 1 2 3 30 102 107 16 sge0f1o ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∖ { ∅ } ) ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝐶𝑍 ) ↦ 𝐷 ) ) )
109 7 eqcomd ( ( 𝜑𝑛𝐶 ) → 𝐺 = ( 𝐹𝑛 ) )
110 109 34 eqeltrd ( ( 𝜑𝑛𝐶 ) → 𝐺𝐴 )
111 105 44 110 syl2anc ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) → 𝐺𝐴 )
112 111 ex ( 𝜑 → ( 𝑛 ∈ ( 𝐶𝑍 ) → 𝐺𝐴 ) )
113 112 imdistani ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) → ( 𝜑𝐺𝐴 ) )
114 nfcv 𝑘 𝐺
115 nfv 𝑘 𝐺𝐴
116 1 115 nfan 𝑘 ( 𝜑𝐺𝐴 )
117 nfv 𝑘 𝐷 ∈ ( 0 [,] +∞ )
118 116 117 nfim 𝑘 ( ( 𝜑𝐺𝐴 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
119 eleq1 ( 𝑘 = 𝐺 → ( 𝑘𝐴𝐺𝐴 ) )
120 119 anbi2d ( 𝑘 = 𝐺 → ( ( 𝜑𝑘𝐴 ) ↔ ( 𝜑𝐺𝐴 ) ) )
121 3 eleq1d ( 𝑘 = 𝐺 → ( 𝐵 ∈ ( 0 [,] +∞ ) ↔ 𝐷 ∈ ( 0 [,] +∞ ) ) )
122 120 121 imbi12d ( 𝑘 = 𝐺 → ( ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) ) ↔ ( ( 𝜑𝐺𝐴 ) → 𝐷 ∈ ( 0 [,] +∞ ) ) ) )
123 114 118 122 8 vtoclgf ( 𝐺𝐴 → ( ( 𝜑𝐺𝐴 ) → 𝐷 ∈ ( 0 [,] +∞ ) ) )
124 111 113 123 sylc ( ( 𝜑𝑛 ∈ ( 𝐶𝑍 ) ) → 𝐷 ∈ ( 0 [,] +∞ ) )
125 simpl ( ( 𝜑𝑛 ∈ ( 𝐶 ∖ ( 𝐶𝑍 ) ) ) → 𝜑 )
126 eldifi ( 𝑛 ∈ ( 𝐶 ∖ ( 𝐶𝑍 ) ) → 𝑛𝐶 )
127 126 adantl ( ( 𝜑𝑛 ∈ ( 𝐶 ∖ ( 𝐶𝑍 ) ) ) → 𝑛𝐶 )
128 125 127 110 syl2anc ( ( 𝜑𝑛 ∈ ( 𝐶 ∖ ( 𝐶𝑍 ) ) ) → 𝐺𝐴 )
129 dfin4 ( 𝑍𝐶 ) = ( 𝑍 ∖ ( 𝑍𝐶 ) )
130 difss ( 𝑍 ∖ ( 𝑍𝐶 ) ) ⊆ 𝑍
131 129 130 eqsstri ( 𝑍𝐶 ) ⊆ 𝑍
132 inss2 ( 𝐶𝑍 ) ⊆ 𝑍
133 id ( 𝑛 ∈ ( 𝐶 ∖ ( 𝐶𝑍 ) ) → 𝑛 ∈ ( 𝐶 ∖ ( 𝐶𝑍 ) ) )
134 dfin4 ( 𝐶𝑍 ) = ( 𝐶 ∖ ( 𝐶𝑍 ) )
135 134 eqcomi ( 𝐶 ∖ ( 𝐶𝑍 ) ) = ( 𝐶𝑍 )
136 133 135 eleqtrdi ( 𝑛 ∈ ( 𝐶 ∖ ( 𝐶𝑍 ) ) → 𝑛 ∈ ( 𝐶𝑍 ) )
137 132 136 sseldi ( 𝑛 ∈ ( 𝐶 ∖ ( 𝐶𝑍 ) ) → 𝑛𝑍 )
138 137 126 elind ( 𝑛 ∈ ( 𝐶 ∖ ( 𝐶𝑍 ) ) → 𝑛 ∈ ( 𝑍𝐶 ) )
139 131 138 sseldi ( 𝑛 ∈ ( 𝐶 ∖ ( 𝐶𝑍 ) ) → 𝑛𝑍 )
140 139 adantl ( ( 𝜑𝑛 ∈ ( 𝐶 ∖ ( 𝐶𝑍 ) ) ) → 𝑛𝑍 )
141 77 eqcomd ( ( 𝜑𝑛𝑍 ) → ∅ = ( 𝐹𝑛 ) )
142 simpl ( ( 𝜑𝑛𝑍 ) → 𝜑 )
143 74 simpld ( ( 𝜑𝑛𝑍 ) → 𝑛𝐶 )
144 142 143 7 syl2anc ( ( 𝜑𝑛𝑍 ) → ( 𝐹𝑛 ) = 𝐺 )
145 141 144 eqtr2d ( ( 𝜑𝑛𝑍 ) → 𝐺 = ∅ )
146 125 140 145 syl2anc ( ( 𝜑𝑛 ∈ ( 𝐶 ∖ ( 𝐶𝑍 ) ) ) → 𝐺 = ∅ )
147 125 146 jca ( ( 𝜑𝑛 ∈ ( 𝐶 ∖ ( 𝐶𝑍 ) ) ) → ( 𝜑𝐺 = ∅ ) )
148 nfv 𝑘 𝐺 = ∅
149 1 148 nfan 𝑘 ( 𝜑𝐺 = ∅ )
150 nfv 𝑘 𝐷 = 0
151 149 150 nfim 𝑘 ( ( 𝜑𝐺 = ∅ ) → 𝐷 = 0 )
152 eqeq1 ( 𝑘 = 𝐺 → ( 𝑘 = ∅ ↔ 𝐺 = ∅ ) )
153 152 anbi2d ( 𝑘 = 𝐺 → ( ( 𝜑𝑘 = ∅ ) ↔ ( 𝜑𝐺 = ∅ ) ) )
154 3 eqeq1d ( 𝑘 = 𝐺 → ( 𝐵 = 0 ↔ 𝐷 = 0 ) )
155 153 154 imbi12d ( 𝑘 = 𝐺 → ( ( ( 𝜑𝑘 = ∅ ) → 𝐵 = 0 ) ↔ ( ( 𝜑𝐺 = ∅ ) → 𝐷 = 0 ) ) )
156 114 151 155 9 vtoclgf ( 𝐺𝐴 → ( ( 𝜑𝐺 = ∅ ) → 𝐷 = 0 ) )
157 128 147 156 sylc ( ( 𝜑𝑛 ∈ ( 𝐶 ∖ ( 𝐶𝑍 ) ) ) → 𝐷 = 0 )
158 2 4 43 124 157 sge0ss ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ( 𝐶𝑍 ) ↦ 𝐷 ) ) = ( Σ^ ‘ ( 𝑛𝐶𝐷 ) ) )
159 29 108 158 3eqtrd ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐵 ) ) = ( Σ^ ‘ ( 𝑛𝐶𝐷 ) ) )