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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑗 ) ∈ 𝑆 )
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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑗 ) ∈ 𝑆 )
54 50 53 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ( 𝑀 ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ( 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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑖 ) ∈ 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 𝐺 ) ) = ( Σ^ ‘ ( 𝑀 ∘ 𝐺 ) ) )