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 𝐺 ) ) = ( Σ^ ‘ ( 𝑀 ∘ 𝐺 ) ) ) |