Metamath Proof Explorer


Theorem meadjiunlem

Description: The sum of nonnegative extended reals, restricted to the range of another function. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses meadjiunlem.f ( 𝜑𝑀 ∈ Meas )
meadjiunlem.3 𝑆 = dom 𝑀
meadjiunlem.x ( 𝜑𝑋𝑉 )
meadjiunlem.g ( 𝜑𝐺 : 𝑋𝑆 )
meadjiunlem.y 𝑌 = { 𝑖𝑋 ∣ ( 𝐺𝑖 ) ≠ ∅ }
meadjiunlem.dj ( 𝜑Disj 𝑖𝑋 ( 𝐺𝑖 ) )
Assertion meadjiunlem ( 𝜑 → ( Σ^ ‘ ( 𝑀 ↾ ran 𝐺 ) ) = ( Σ^ ‘ ( 𝑀𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 meadjiunlem.f ( 𝜑𝑀 ∈ Meas )
2 meadjiunlem.3 𝑆 = dom 𝑀
3 meadjiunlem.x ( 𝜑𝑋𝑉 )
4 meadjiunlem.g ( 𝜑𝐺 : 𝑋𝑆 )
5 meadjiunlem.y 𝑌 = { 𝑖𝑋 ∣ ( 𝐺𝑖 ) ≠ ∅ }
6 meadjiunlem.dj ( 𝜑Disj 𝑖𝑋 ( 𝐺𝑖 ) )
7 nfv 𝑘 𝜑
8 4 3 jca ( 𝜑 → ( 𝐺 : 𝑋𝑆𝑋𝑉 ) )
9 fex ( ( 𝐺 : 𝑋𝑆𝑋𝑉 ) → 𝐺 ∈ V )
10 rnexg ( 𝐺 ∈ V → ran 𝐺 ∈ V )
11 8 9 10 3syl ( 𝜑 → ran 𝐺 ∈ V )
12 difssd ( 𝜑 → ( ran 𝐺 ∖ { ∅ } ) ⊆ ran 𝐺 )
13 1 2 meaf ( 𝜑𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
14 13 adantr ( ( 𝜑𝑘 ∈ ( ran 𝐺 ∖ { ∅ } ) ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
15 4 frnd ( 𝜑 → ran 𝐺𝑆 )
16 15 adantr ( ( 𝜑𝑘 ∈ ( ran 𝐺 ∖ { ∅ } ) ) → ran 𝐺𝑆 )
17 12 sselda ( ( 𝜑𝑘 ∈ ( ran 𝐺 ∖ { ∅ } ) ) → 𝑘 ∈ ran 𝐺 )
18 16 17 sseldd ( ( 𝜑𝑘 ∈ ( ran 𝐺 ∖ { ∅ } ) ) → 𝑘𝑆 )
19 14 18 ffvelrnd ( ( 𝜑𝑘 ∈ ( ran 𝐺 ∖ { ∅ } ) ) → ( 𝑀𝑘 ) ∈ ( 0 [,] +∞ ) )
20 simpl ( ( 𝜑𝑘 ∈ ( ran 𝐺 ∖ ( ran 𝐺 ∖ { ∅ } ) ) ) → 𝜑 )
21 id ( 𝑘 ∈ ( ran 𝐺 ∖ ( ran 𝐺 ∖ { ∅ } ) ) → 𝑘 ∈ ( ran 𝐺 ∖ ( ran 𝐺 ∖ { ∅ } ) ) )
22 dfin4 ( ran 𝐺 ∩ { ∅ } ) = ( ran 𝐺 ∖ ( ran 𝐺 ∖ { ∅ } ) )
23 22 eqcomi ( ran 𝐺 ∖ ( ran 𝐺 ∖ { ∅ } ) ) = ( ran 𝐺 ∩ { ∅ } )
24 21 23 eleqtrdi ( 𝑘 ∈ ( ran 𝐺 ∖ ( ran 𝐺 ∖ { ∅ } ) ) → 𝑘 ∈ ( ran 𝐺 ∩ { ∅ } ) )
25 elinel2 ( 𝑘 ∈ ( ran 𝐺 ∩ { ∅ } ) → 𝑘 ∈ { ∅ } )
26 elsni ( 𝑘 ∈ { ∅ } → 𝑘 = ∅ )
27 25 26 syl ( 𝑘 ∈ ( ran 𝐺 ∩ { ∅ } ) → 𝑘 = ∅ )
28 24 27 syl ( 𝑘 ∈ ( ran 𝐺 ∖ ( ran 𝐺 ∖ { ∅ } ) ) → 𝑘 = ∅ )
29 28 adantl ( ( 𝜑𝑘 ∈ ( ran 𝐺 ∖ ( ran 𝐺 ∖ { ∅ } ) ) ) → 𝑘 = ∅ )
30 simpr ( ( 𝜑𝑘 = ∅ ) → 𝑘 = ∅ )
31 30 fveq2d ( ( 𝜑𝑘 = ∅ ) → ( 𝑀𝑘 ) = ( 𝑀 ‘ ∅ ) )
32 1 mea0 ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
33 32 adantr ( ( 𝜑𝑘 = ∅ ) → ( 𝑀 ‘ ∅ ) = 0 )
34 31 33 eqtrd ( ( 𝜑𝑘 = ∅ ) → ( 𝑀𝑘 ) = 0 )
35 20 29 34 syl2anc ( ( 𝜑𝑘 ∈ ( ran 𝐺 ∖ ( ran 𝐺 ∖ { ∅ } ) ) ) → ( 𝑀𝑘 ) = 0 )
36 7 11 12 19 35 sge0ss ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( ran 𝐺 ∖ { ∅ } ) ↦ ( 𝑀𝑘 ) ) ) = ( Σ^ ‘ ( 𝑘 ∈ ran 𝐺 ↦ ( 𝑀𝑘 ) ) ) )
37 36 eqcomd ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ran 𝐺 ↦ ( 𝑀𝑘 ) ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( ran 𝐺 ∖ { ∅ } ) ↦ ( 𝑀𝑘 ) ) ) )
38 13 15 feqresmpt ( 𝜑 → ( 𝑀 ↾ ran 𝐺 ) = ( 𝑘 ∈ ran 𝐺 ↦ ( 𝑀𝑘 ) ) )
39 38 fveq2d ( 𝜑 → ( Σ^ ‘ ( 𝑀 ↾ ran 𝐺 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ran 𝐺 ↦ ( 𝑀𝑘 ) ) ) )
40 4 ffvelrnda ( ( 𝜑𝑗𝑋 ) → ( 𝐺𝑗 ) ∈ 𝑆 )
41 4 feqmptd ( 𝜑𝐺 = ( 𝑗𝑋 ↦ ( 𝐺𝑗 ) ) )
42 13 feqmptd ( 𝜑𝑀 = ( 𝑘𝑆 ↦ ( 𝑀𝑘 ) ) )
43 fveq2 ( 𝑘 = ( 𝐺𝑗 ) → ( 𝑀𝑘 ) = ( 𝑀 ‘ ( 𝐺𝑗 ) ) )
44 40 41 42 43 fmptco ( 𝜑 → ( 𝑀𝐺 ) = ( 𝑗𝑋 ↦ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ) )
45 44 fveq2d ( 𝜑 → ( Σ^ ‘ ( 𝑀𝐺 ) ) = ( Σ^ ‘ ( 𝑗𝑋 ↦ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ) ) )
46 nfv 𝑗 𝜑
47 ssrab2 { 𝑖𝑋 ∣ ( 𝐺𝑖 ) ≠ ∅ } ⊆ 𝑋
48 47 a1i ( 𝜑 → { 𝑖𝑋 ∣ ( 𝐺𝑖 ) ≠ ∅ } ⊆ 𝑋 )
49 5 48 eqsstrid ( 𝜑𝑌𝑋 )
50 13 adantr ( ( 𝜑𝑗𝑌 ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
51 4 adantr ( ( 𝜑𝑗𝑌 ) → 𝐺 : 𝑋𝑆 )
52 49 sselda ( ( 𝜑𝑗𝑌 ) → 𝑗𝑋 )
53 51 52 ffvelrnd ( ( 𝜑𝑗𝑌 ) → ( 𝐺𝑗 ) ∈ 𝑆 )
54 50 53 ffvelrnd ( ( 𝜑𝑗𝑌 ) → ( 𝑀 ‘ ( 𝐺𝑗 ) ) ∈ ( 0 [,] +∞ ) )
55 eldifi ( 𝑗 ∈ ( 𝑋𝑌 ) → 𝑗𝑋 )
56 55 ad2antlr ( ( ( 𝜑𝑗 ∈ ( 𝑋𝑌 ) ) ∧ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ≠ 0 ) → 𝑗𝑋 )
57 fveq2 ( ( 𝐺𝑗 ) = ∅ → ( 𝑀 ‘ ( 𝐺𝑗 ) ) = ( 𝑀 ‘ ∅ ) )
58 57 adantl ( ( 𝜑 ∧ ( 𝐺𝑗 ) = ∅ ) → ( 𝑀 ‘ ( 𝐺𝑗 ) ) = ( 𝑀 ‘ ∅ ) )
59 1 adantr ( ( 𝜑 ∧ ( 𝐺𝑗 ) = ∅ ) → 𝑀 ∈ Meas )
60 59 mea0 ( ( 𝜑 ∧ ( 𝐺𝑗 ) = ∅ ) → ( 𝑀 ‘ ∅ ) = 0 )
61 58 60 eqtrd ( ( 𝜑 ∧ ( 𝐺𝑗 ) = ∅ ) → ( 𝑀 ‘ ( 𝐺𝑗 ) ) = 0 )
62 61 ad4ant14 ( ( ( ( 𝜑𝑗 ∈ ( 𝑋𝑌 ) ) ∧ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ≠ 0 ) ∧ ( 𝐺𝑗 ) = ∅ ) → ( 𝑀 ‘ ( 𝐺𝑗 ) ) = 0 )
63 neneq ( ( 𝑀 ‘ ( 𝐺𝑗 ) ) ≠ 0 → ¬ ( 𝑀 ‘ ( 𝐺𝑗 ) ) = 0 )
64 63 ad2antlr ( ( ( ( 𝜑𝑗 ∈ ( 𝑋𝑌 ) ) ∧ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ≠ 0 ) ∧ ( 𝐺𝑗 ) = ∅ ) → ¬ ( 𝑀 ‘ ( 𝐺𝑗 ) ) = 0 )
65 62 64 pm2.65da ( ( ( 𝜑𝑗 ∈ ( 𝑋𝑌 ) ) ∧ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ≠ 0 ) → ¬ ( 𝐺𝑗 ) = ∅ )
66 65 neqned ( ( ( 𝜑𝑗 ∈ ( 𝑋𝑌 ) ) ∧ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ≠ 0 ) → ( 𝐺𝑗 ) ≠ ∅ )
67 56 66 jca ( ( ( 𝜑𝑗 ∈ ( 𝑋𝑌 ) ) ∧ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ≠ 0 ) → ( 𝑗𝑋 ∧ ( 𝐺𝑗 ) ≠ ∅ ) )
68 fveq2 ( 𝑖 = 𝑗 → ( 𝐺𝑖 ) = ( 𝐺𝑗 ) )
69 68 neeq1d ( 𝑖 = 𝑗 → ( ( 𝐺𝑖 ) ≠ ∅ ↔ ( 𝐺𝑗 ) ≠ ∅ ) )
70 69 elrab ( 𝑗 ∈ { 𝑖𝑋 ∣ ( 𝐺𝑖 ) ≠ ∅ } ↔ ( 𝑗𝑋 ∧ ( 𝐺𝑗 ) ≠ ∅ ) )
71 67 70 sylibr ( ( ( 𝜑𝑗 ∈ ( 𝑋𝑌 ) ) ∧ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ≠ 0 ) → 𝑗 ∈ { 𝑖𝑋 ∣ ( 𝐺𝑖 ) ≠ ∅ } )
72 71 5 eleqtrrdi ( ( ( 𝜑𝑗 ∈ ( 𝑋𝑌 ) ) ∧ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ≠ 0 ) → 𝑗𝑌 )
73 eldifn ( 𝑗 ∈ ( 𝑋𝑌 ) → ¬ 𝑗𝑌 )
74 73 ad2antlr ( ( ( 𝜑𝑗 ∈ ( 𝑋𝑌 ) ) ∧ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ≠ 0 ) → ¬ 𝑗𝑌 )
75 72 74 pm2.65da ( ( 𝜑𝑗 ∈ ( 𝑋𝑌 ) ) → ¬ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ≠ 0 )
76 nne ( ¬ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ≠ 0 ↔ ( 𝑀 ‘ ( 𝐺𝑗 ) ) = 0 )
77 75 76 sylib ( ( 𝜑𝑗 ∈ ( 𝑋𝑌 ) ) → ( 𝑀 ‘ ( 𝐺𝑗 ) ) = 0 )
78 46 3 49 54 77 sge0ss ( 𝜑 → ( Σ^ ‘ ( 𝑗𝑌 ↦ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗𝑋 ↦ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ) ) )
79 78 eqcomd ( 𝜑 → ( Σ^ ‘ ( 𝑗𝑋 ↦ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗𝑌 ↦ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ) ) )
80 3 49 ssexd ( 𝜑𝑌 ∈ V )
81 nfv 𝑖 𝜑
82 eqid ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) ) = ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) )
83 4 ffnd ( 𝜑𝐺 Fn 𝑋 )
84 dffn3 ( 𝐺 Fn 𝑋𝐺 : 𝑋 ⟶ ran 𝐺 )
85 83 84 sylib ( 𝜑𝐺 : 𝑋 ⟶ ran 𝐺 )
86 85 adantr ( ( 𝜑𝑖𝑌 ) → 𝐺 : 𝑋 ⟶ ran 𝐺 )
87 49 sselda ( ( 𝜑𝑖𝑌 ) → 𝑖𝑋 )
88 86 87 ffvelrnd ( ( 𝜑𝑖𝑌 ) → ( 𝐺𝑖 ) ∈ ran 𝐺 )
89 5 eleq2i ( 𝑖𝑌𝑖 ∈ { 𝑖𝑋 ∣ ( 𝐺𝑖 ) ≠ ∅ } )
90 rabid ( 𝑖 ∈ { 𝑖𝑋 ∣ ( 𝐺𝑖 ) ≠ ∅ } ↔ ( 𝑖𝑋 ∧ ( 𝐺𝑖 ) ≠ ∅ ) )
91 89 90 bitri ( 𝑖𝑌 ↔ ( 𝑖𝑋 ∧ ( 𝐺𝑖 ) ≠ ∅ ) )
92 91 biimpi ( 𝑖𝑌 → ( 𝑖𝑋 ∧ ( 𝐺𝑖 ) ≠ ∅ ) )
93 92 simprd ( 𝑖𝑌 → ( 𝐺𝑖 ) ≠ ∅ )
94 93 adantl ( ( 𝜑𝑖𝑌 ) → ( 𝐺𝑖 ) ≠ ∅ )
95 nelsn ( ( 𝐺𝑖 ) ≠ ∅ → ¬ ( 𝐺𝑖 ) ∈ { ∅ } )
96 94 95 syl ( ( 𝜑𝑖𝑌 ) → ¬ ( 𝐺𝑖 ) ∈ { ∅ } )
97 88 96 eldifd ( ( 𝜑𝑖𝑌 ) → ( 𝐺𝑖 ) ∈ ( ran 𝐺 ∖ { ∅ } ) )
98 disjss1 ( 𝑌𝑋 → ( Disj 𝑖𝑋 ( 𝐺𝑖 ) → Disj 𝑖𝑌 ( 𝐺𝑖 ) ) )
99 49 6 98 sylc ( 𝜑Disj 𝑖𝑌 ( 𝐺𝑖 ) )
100 81 82 97 94 99 disjf1 ( 𝜑 → ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) ) : 𝑌1-1→ ( ran 𝐺 ∖ { ∅ } ) )
101 4 49 feqresmpt ( 𝜑 → ( 𝐺𝑌 ) = ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) ) )
102 f1eq1 ( ( 𝐺𝑌 ) = ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) ) → ( ( 𝐺𝑌 ) : 𝑌1-1→ ( ran 𝐺 ∖ { ∅ } ) ↔ ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) ) : 𝑌1-1→ ( ran 𝐺 ∖ { ∅ } ) ) )
103 101 102 syl ( 𝜑 → ( ( 𝐺𝑌 ) : 𝑌1-1→ ( ran 𝐺 ∖ { ∅ } ) ↔ ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) ) : 𝑌1-1→ ( ran 𝐺 ∖ { ∅ } ) ) )
104 100 103 mpbird ( 𝜑 → ( 𝐺𝑌 ) : 𝑌1-1→ ( ran 𝐺 ∖ { ∅ } ) )
105 101 rneqd ( 𝜑 → ran ( 𝐺𝑌 ) = ran ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) ) )
106 97 ralrimiva ( 𝜑 → ∀ 𝑖𝑌 ( 𝐺𝑖 ) ∈ ( ran 𝐺 ∖ { ∅ } ) )
107 82 rnmptss ( ∀ 𝑖𝑌 ( 𝐺𝑖 ) ∈ ( ran 𝐺 ∖ { ∅ } ) → ran ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) ) ⊆ ( ran 𝐺 ∖ { ∅ } ) )
108 106 107 syl ( 𝜑 → ran ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) ) ⊆ ( ran 𝐺 ∖ { ∅ } ) )
109 105 108 eqsstrd ( 𝜑 → ran ( 𝐺𝑌 ) ⊆ ( ran 𝐺 ∖ { ∅ } ) )
110 simpl ( ( 𝜑𝑥 ∈ ( ran 𝐺 ∖ { ∅ } ) ) → 𝜑 )
111 eldifi ( 𝑥 ∈ ( ran 𝐺 ∖ { ∅ } ) → 𝑥 ∈ ran 𝐺 )
112 111 adantl ( ( 𝜑𝑥 ∈ ( ran 𝐺 ∖ { ∅ } ) ) → 𝑥 ∈ ran 𝐺 )
113 eldifsni ( 𝑥 ∈ ( ran 𝐺 ∖ { ∅ } ) → 𝑥 ≠ ∅ )
114 113 adantl ( ( 𝜑𝑥 ∈ ( ran 𝐺 ∖ { ∅ } ) ) → 𝑥 ≠ ∅ )
115 simpr ( ( 𝜑𝑥 ∈ ran 𝐺 ) → 𝑥 ∈ ran 𝐺 )
116 fvelrnb ( 𝐺 Fn 𝑋 → ( 𝑥 ∈ ran 𝐺 ↔ ∃ 𝑖𝑋 ( 𝐺𝑖 ) = 𝑥 ) )
117 83 116 syl ( 𝜑 → ( 𝑥 ∈ ran 𝐺 ↔ ∃ 𝑖𝑋 ( 𝐺𝑖 ) = 𝑥 ) )
118 117 adantr ( ( 𝜑𝑥 ∈ ran 𝐺 ) → ( 𝑥 ∈ ran 𝐺 ↔ ∃ 𝑖𝑋 ( 𝐺𝑖 ) = 𝑥 ) )
119 115 118 mpbid ( ( 𝜑𝑥 ∈ ran 𝐺 ) → ∃ 𝑖𝑋 ( 𝐺𝑖 ) = 𝑥 )
120 119 3adant3 ( ( 𝜑𝑥 ∈ ran 𝐺𝑥 ≠ ∅ ) → ∃ 𝑖𝑋 ( 𝐺𝑖 ) = 𝑥 )
121 id ( ( 𝐺𝑖 ) = 𝑥 → ( 𝐺𝑖 ) = 𝑥 )
122 121 eqcomd ( ( 𝐺𝑖 ) = 𝑥𝑥 = ( 𝐺𝑖 ) )
123 122 3ad2ant3 ( ( ( 𝜑𝑥 ≠ ∅ ) ∧ 𝑖𝑋 ∧ ( 𝐺𝑖 ) = 𝑥 ) → 𝑥 = ( 𝐺𝑖 ) )
124 simp1l ( ( ( 𝜑𝑥 ≠ ∅ ) ∧ 𝑖𝑋 ∧ ( 𝐺𝑖 ) = 𝑥 ) → 𝜑 )
125 simp2 ( ( ( 𝜑𝑥 ≠ ∅ ) ∧ 𝑖𝑋 ∧ ( 𝐺𝑖 ) = 𝑥 ) → 𝑖𝑋 )
126 simpr ( ( 𝑥 ≠ ∅ ∧ ( 𝐺𝑖 ) = 𝑥 ) → ( 𝐺𝑖 ) = 𝑥 )
127 simpl ( ( 𝑥 ≠ ∅ ∧ ( 𝐺𝑖 ) = 𝑥 ) → 𝑥 ≠ ∅ )
128 126 127 eqnetrd ( ( 𝑥 ≠ ∅ ∧ ( 𝐺𝑖 ) = 𝑥 ) → ( 𝐺𝑖 ) ≠ ∅ )
129 128 adantll ( ( ( 𝜑𝑥 ≠ ∅ ) ∧ ( 𝐺𝑖 ) = 𝑥 ) → ( 𝐺𝑖 ) ≠ ∅ )
130 129 3adant2 ( ( ( 𝜑𝑥 ≠ ∅ ) ∧ 𝑖𝑋 ∧ ( 𝐺𝑖 ) = 𝑥 ) → ( 𝐺𝑖 ) ≠ ∅ )
131 91 biimpri ( ( 𝑖𝑋 ∧ ( 𝐺𝑖 ) ≠ ∅ ) → 𝑖𝑌 )
132 fvexd ( ( 𝑖𝑋 ∧ ( 𝐺𝑖 ) ≠ ∅ ) → ( 𝐺𝑖 ) ∈ V )
133 82 elrnmpt1 ( ( 𝑖𝑌 ∧ ( 𝐺𝑖 ) ∈ V ) → ( 𝐺𝑖 ) ∈ ran ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) ) )
134 131 132 133 syl2anc ( ( 𝑖𝑋 ∧ ( 𝐺𝑖 ) ≠ ∅ ) → ( 𝐺𝑖 ) ∈ ran ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) ) )
135 134 3adant1 ( ( 𝜑𝑖𝑋 ∧ ( 𝐺𝑖 ) ≠ ∅ ) → ( 𝐺𝑖 ) ∈ ran ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) ) )
136 105 eqcomd ( 𝜑 → ran ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) ) = ran ( 𝐺𝑌 ) )
137 136 3ad2ant1 ( ( 𝜑𝑖𝑋 ∧ ( 𝐺𝑖 ) ≠ ∅ ) → ran ( 𝑖𝑌 ↦ ( 𝐺𝑖 ) ) = ran ( 𝐺𝑌 ) )
138 135 137 eleqtrd ( ( 𝜑𝑖𝑋 ∧ ( 𝐺𝑖 ) ≠ ∅ ) → ( 𝐺𝑖 ) ∈ ran ( 𝐺𝑌 ) )
139 124 125 130 138 syl3anc ( ( ( 𝜑𝑥 ≠ ∅ ) ∧ 𝑖𝑋 ∧ ( 𝐺𝑖 ) = 𝑥 ) → ( 𝐺𝑖 ) ∈ ran ( 𝐺𝑌 ) )
140 123 139 eqeltrd ( ( ( 𝜑𝑥 ≠ ∅ ) ∧ 𝑖𝑋 ∧ ( 𝐺𝑖 ) = 𝑥 ) → 𝑥 ∈ ran ( 𝐺𝑌 ) )
141 140 3exp ( ( 𝜑𝑥 ≠ ∅ ) → ( 𝑖𝑋 → ( ( 𝐺𝑖 ) = 𝑥𝑥 ∈ ran ( 𝐺𝑌 ) ) ) )
142 141 rexlimdv ( ( 𝜑𝑥 ≠ ∅ ) → ( ∃ 𝑖𝑋 ( 𝐺𝑖 ) = 𝑥𝑥 ∈ ran ( 𝐺𝑌 ) ) )
143 142 3adant2 ( ( 𝜑𝑥 ∈ ran 𝐺𝑥 ≠ ∅ ) → ( ∃ 𝑖𝑋 ( 𝐺𝑖 ) = 𝑥𝑥 ∈ ran ( 𝐺𝑌 ) ) )
144 120 143 mpd ( ( 𝜑𝑥 ∈ ran 𝐺𝑥 ≠ ∅ ) → 𝑥 ∈ ran ( 𝐺𝑌 ) )
145 110 112 114 144 syl3anc ( ( 𝜑𝑥 ∈ ( ran 𝐺 ∖ { ∅ } ) ) → 𝑥 ∈ ran ( 𝐺𝑌 ) )
146 109 145 eqelssd ( 𝜑 → ran ( 𝐺𝑌 ) = ( ran 𝐺 ∖ { ∅ } ) )
147 104 146 jca ( 𝜑 → ( ( 𝐺𝑌 ) : 𝑌1-1→ ( ran 𝐺 ∖ { ∅ } ) ∧ ran ( 𝐺𝑌 ) = ( ran 𝐺 ∖ { ∅ } ) ) )
148 dff1o5 ( ( 𝐺𝑌 ) : 𝑌1-1-onto→ ( ran 𝐺 ∖ { ∅ } ) ↔ ( ( 𝐺𝑌 ) : 𝑌1-1→ ( ran 𝐺 ∖ { ∅ } ) ∧ ran ( 𝐺𝑌 ) = ( ran 𝐺 ∖ { ∅ } ) ) )
149 147 148 sylibr ( 𝜑 → ( 𝐺𝑌 ) : 𝑌1-1-onto→ ( ran 𝐺 ∖ { ∅ } ) )
150 fvres ( 𝑗𝑌 → ( ( 𝐺𝑌 ) ‘ 𝑗 ) = ( 𝐺𝑗 ) )
151 150 adantl ( ( 𝜑𝑗𝑌 ) → ( ( 𝐺𝑌 ) ‘ 𝑗 ) = ( 𝐺𝑗 ) )
152 7 46 43 80 149 151 19 sge0f1o ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( ran 𝐺 ∖ { ∅ } ) ↦ ( 𝑀𝑘 ) ) ) = ( Σ^ ‘ ( 𝑗𝑌 ↦ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ) ) )
153 152 eqcomd ( 𝜑 → ( Σ^ ‘ ( 𝑗𝑌 ↦ ( 𝑀 ‘ ( 𝐺𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( ran 𝐺 ∖ { ∅ } ) ↦ ( 𝑀𝑘 ) ) ) )
154 45 79 153 3eqtrd ( 𝜑 → ( Σ^ ‘ ( 𝑀𝐺 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( ran 𝐺 ∖ { ∅ } ) ↦ ( 𝑀𝑘 ) ) ) )
155 37 39 154 3eqtr4d ( 𝜑 → ( Σ^ ‘ ( 𝑀 ↾ ran 𝐺 ) ) = ( Σ^ ‘ ( 𝑀𝐺 ) ) )