Step | Hyp | Ref
| Expression |
1 | | gsumle.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
2 | | ssid 3899 |
. . . 4
⊢ 𝐴 ⊆ 𝐴 |
3 | | sseq1 3902 |
. . . . . . . 8
⊢ (𝑎 = ∅ → (𝑎 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
4 | 3 | anbi2d 632 |
. . . . . . 7
⊢ (𝑎 = ∅ → ((𝜑 ∧ 𝑎 ⊆ 𝐴) ↔ (𝜑 ∧ ∅ ⊆ 𝐴))) |
5 | | reseq2 5820 |
. . . . . . . . 9
⊢ (𝑎 = ∅ → (𝐹 ↾ 𝑎) = (𝐹 ↾ ∅)) |
6 | 5 | oveq2d 7186 |
. . . . . . . 8
⊢ (𝑎 = ∅ → (𝑀 Σg
(𝐹 ↾ 𝑎)) = (𝑀 Σg (𝐹 ↾
∅))) |
7 | | reseq2 5820 |
. . . . . . . . 9
⊢ (𝑎 = ∅ → (𝐺 ↾ 𝑎) = (𝐺 ↾ ∅)) |
8 | 7 | oveq2d 7186 |
. . . . . . . 8
⊢ (𝑎 = ∅ → (𝑀 Σg
(𝐺 ↾ 𝑎)) = (𝑀 Σg (𝐺 ↾
∅))) |
9 | 6, 8 | breq12d 5043 |
. . . . . . 7
⊢ (𝑎 = ∅ → ((𝑀 Σg
(𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎)) ↔ (𝑀 Σg (𝐹 ↾ ∅)) ≤ (𝑀 Σg
(𝐺 ↾
∅)))) |
10 | 4, 9 | imbi12d 348 |
. . . . . 6
⊢ (𝑎 = ∅ → (((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎))) ↔ ((𝜑 ∧ ∅ ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ ∅)) ≤ (𝑀 Σg
(𝐺 ↾
∅))))) |
11 | | sseq1 3902 |
. . . . . . . 8
⊢ (𝑎 = 𝑒 → (𝑎 ⊆ 𝐴 ↔ 𝑒 ⊆ 𝐴)) |
12 | 11 | anbi2d 632 |
. . . . . . 7
⊢ (𝑎 = 𝑒 → ((𝜑 ∧ 𝑎 ⊆ 𝐴) ↔ (𝜑 ∧ 𝑒 ⊆ 𝐴))) |
13 | | reseq2 5820 |
. . . . . . . . 9
⊢ (𝑎 = 𝑒 → (𝐹 ↾ 𝑎) = (𝐹 ↾ 𝑒)) |
14 | 13 | oveq2d 7186 |
. . . . . . . 8
⊢ (𝑎 = 𝑒 → (𝑀 Σg (𝐹 ↾ 𝑎)) = (𝑀 Σg (𝐹 ↾ 𝑒))) |
15 | | reseq2 5820 |
. . . . . . . . 9
⊢ (𝑎 = 𝑒 → (𝐺 ↾ 𝑎) = (𝐺 ↾ 𝑒)) |
16 | 15 | oveq2d 7186 |
. . . . . . . 8
⊢ (𝑎 = 𝑒 → (𝑀 Σg (𝐺 ↾ 𝑎)) = (𝑀 Σg (𝐺 ↾ 𝑒))) |
17 | 14, 16 | breq12d 5043 |
. . . . . . 7
⊢ (𝑎 = 𝑒 → ((𝑀 Σg (𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎)) ↔ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒)))) |
18 | 12, 17 | imbi12d 348 |
. . . . . 6
⊢ (𝑎 = 𝑒 → (((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎))) ↔ ((𝜑 ∧ 𝑒 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))))) |
19 | | sseq1 3902 |
. . . . . . . 8
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → (𝑎 ⊆ 𝐴 ↔ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) |
20 | 19 | anbi2d 632 |
. . . . . . 7
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → ((𝜑 ∧ 𝑎 ⊆ 𝐴) ↔ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴))) |
21 | | reseq2 5820 |
. . . . . . . . 9
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → (𝐹 ↾ 𝑎) = (𝐹 ↾ (𝑒 ∪ {𝑦}))) |
22 | 21 | oveq2d 7186 |
. . . . . . . 8
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → (𝑀 Σg (𝐹 ↾ 𝑎)) = (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦})))) |
23 | | reseq2 5820 |
. . . . . . . . 9
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → (𝐺 ↾ 𝑎) = (𝐺 ↾ (𝑒 ∪ {𝑦}))) |
24 | 23 | oveq2d 7186 |
. . . . . . . 8
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → (𝑀 Σg (𝐺 ↾ 𝑎)) = (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))) |
25 | 22, 24 | breq12d 5043 |
. . . . . . 7
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → ((𝑀 Σg (𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎)) ↔ (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) ≤ (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))) |
26 | 20, 25 | imbi12d 348 |
. . . . . 6
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → (((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎))) ↔ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) ≤ (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))))) |
27 | | sseq1 3902 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑎 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
28 | 27 | anbi2d 632 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝜑 ∧ 𝑎 ⊆ 𝐴) ↔ (𝜑 ∧ 𝐴 ⊆ 𝐴))) |
29 | | reseq2 5820 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (𝐹 ↾ 𝑎) = (𝐹 ↾ 𝐴)) |
30 | 29 | oveq2d 7186 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑀 Σg (𝐹 ↾ 𝑎)) = (𝑀 Σg (𝐹 ↾ 𝐴))) |
31 | | reseq2 5820 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (𝐺 ↾ 𝑎) = (𝐺 ↾ 𝐴)) |
32 | 31 | oveq2d 7186 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑀 Σg (𝐺 ↾ 𝑎)) = (𝑀 Σg (𝐺 ↾ 𝐴))) |
33 | 30, 32 | breq12d 5043 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝑀 Σg (𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎)) ↔ (𝑀 Σg (𝐹 ↾ 𝐴)) ≤ (𝑀 Σg (𝐺 ↾ 𝐴)))) |
34 | 28, 33 | imbi12d 348 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎))) ↔ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝐴)) ≤ (𝑀 Σg (𝐺 ↾ 𝐴))))) |
35 | | gsumle.m |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ oMnd) |
36 | | omndtos 30908 |
. . . . . . . . . 10
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset) |
37 | | tospos 30818 |
. . . . . . . . . 10
⊢ (𝑀 ∈ Toset → 𝑀 ∈ Poset) |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ Poset) |
39 | | res0 5829 |
. . . . . . . . . . . 12
⊢ (𝐹 ↾ ∅) =
∅ |
40 | 39 | oveq2i 7181 |
. . . . . . . . . . 11
⊢ (𝑀 Σg
(𝐹 ↾ ∅)) =
(𝑀
Σg ∅) |
41 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(0g‘𝑀) = (0g‘𝑀) |
42 | 41 | gsum0 18010 |
. . . . . . . . . . 11
⊢ (𝑀 Σg
∅) = (0g‘𝑀) |
43 | 40, 42 | eqtri 2761 |
. . . . . . . . . 10
⊢ (𝑀 Σg
(𝐹 ↾ ∅)) =
(0g‘𝑀) |
44 | | omndmnd 30907 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Mnd) |
45 | | gsumle.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝑀) |
46 | 45, 41 | mndidcl 18042 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ Mnd →
(0g‘𝑀)
∈ 𝐵) |
47 | 35, 44, 46 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (0g‘𝑀) ∈ 𝐵) |
48 | 43, 47 | eqeltrid 2837 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) ∈ 𝐵) |
49 | | gsumle.l |
. . . . . . . . . 10
⊢ ≤ =
(le‘𝑀) |
50 | 45, 49 | posref 17677 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Poset ∧ (𝑀 Σg
(𝐹 ↾ ∅)) ∈
𝐵) → (𝑀 Σg
(𝐹 ↾ ∅)) ≤ (𝑀 Σg
(𝐹 ↾
∅))) |
51 | 38, 48, 50 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) ≤ (𝑀 Σg
(𝐹 ↾
∅))) |
52 | | res0 5829 |
. . . . . . . . . 10
⊢ (𝐺 ↾ ∅) =
∅ |
53 | 39, 52 | eqtr4i 2764 |
. . . . . . . . 9
⊢ (𝐹 ↾ ∅) = (𝐺 ↾
∅) |
54 | 53 | oveq2i 7181 |
. . . . . . . 8
⊢ (𝑀 Σg
(𝐹 ↾ ∅)) =
(𝑀
Σg (𝐺 ↾ ∅)) |
55 | 51, 54 | breqtrdi 5071 |
. . . . . . 7
⊢ (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) ≤ (𝑀 Σg
(𝐺 ↾
∅))) |
56 | 55 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ ∅ ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ ∅)) ≤ (𝑀 Σg
(𝐺 ↾
∅))) |
57 | | ssun1 4062 |
. . . . . . . . . 10
⊢ 𝑒 ⊆ (𝑒 ∪ {𝑦}) |
58 | | sstr2 3884 |
. . . . . . . . . 10
⊢ (𝑒 ⊆ (𝑒 ∪ {𝑦}) → ((𝑒 ∪ {𝑦}) ⊆ 𝐴 → 𝑒 ⊆ 𝐴)) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑒 ∪ {𝑦}) ⊆ 𝐴 → 𝑒 ⊆ 𝐴) |
60 | 59 | anim2i 620 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝜑 ∧ 𝑒 ⊆ 𝐴)) |
61 | 60 | imim1i 63 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒)))) |
62 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) |
63 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → ¬ 𝑦 ∈ 𝑒) |
64 | | simpr 488 |
. . . . . . . . . 10
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) |
65 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(+g‘𝑀) = (+g‘𝑀) |
66 | 35 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → 𝑀 ∈ oMnd) |
67 | | gsumle.g |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺:𝐴⟶𝐵) |
68 | 67 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝐺:𝐴⟶𝐵) |
69 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑒 ∪ {𝑦}) ⊆ 𝐴) |
70 | | ssun2 4063 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑦} ⊆ (𝑒 ∪ {𝑦}) |
71 | | vex 3402 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V |
72 | 71 | snss 4674 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (𝑒 ∪ {𝑦}) ↔ {𝑦} ⊆ (𝑒 ∪ {𝑦})) |
73 | 70, 72 | mpbir 234 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ (𝑒 ∪ {𝑦}) |
74 | 73 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑦 ∈ (𝑒 ∪ {𝑦})) |
75 | 69, 74 | sseldd 3878 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑦 ∈ 𝐴) |
76 | 68, 75 | ffvelrnd 6862 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐺‘𝑦) ∈ 𝐵) |
77 | 76 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝐺‘𝑦) ∈ 𝐵) |
78 | | gsumle.n |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ CMnd) |
79 | 78 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑀 ∈ CMnd) |
80 | | vex 3402 |
. . . . . . . . . . . . . . 15
⊢ 𝑒 ∈ V |
81 | 80 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑒 ∈ V) |
82 | | gsumle.f |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
83 | 82 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝐹:𝐴⟶𝐵) |
84 | 57, 69 | sstrid 3888 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑒 ⊆ 𝐴) |
85 | 83, 84 | fssresd 6545 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐹 ↾ 𝑒):𝑒⟶𝐵) |
86 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝐴 ∈ Fin) |
87 | | fvexd 6689 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (0g‘𝑀) ∈ V) |
88 | 83, 86, 87 | fdmfifsupp 8916 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝐹 finSupp (0g‘𝑀)) |
89 | 88, 87 | fsuppres 8931 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐹 ↾ 𝑒) finSupp (0g‘𝑀)) |
90 | 45, 41, 79, 81, 85, 89 | gsumcl 19154 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐹 ↾ 𝑒)) ∈ 𝐵) |
91 | 90 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐹 ↾ 𝑒)) ∈ 𝐵) |
92 | 83, 75 | ffvelrnd 6862 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐹‘𝑦) ∈ 𝐵) |
93 | 92 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝐹‘𝑦) ∈ 𝐵) |
94 | 68, 84 | fssresd 6545 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐺 ↾ 𝑒):𝑒⟶𝐵) |
95 | | ssfi 8772 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ Fin ∧ 𝑒 ⊆ 𝐴) → 𝑒 ∈ Fin) |
96 | 86, 84, 95 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑒 ∈ Fin) |
97 | 94, 96, 87 | fdmfifsupp 8916 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐺 ↾ 𝑒) finSupp (0g‘𝑀)) |
98 | 45, 41, 79, 81, 94, 97 | gsumcl 19154 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐺 ↾ 𝑒)) ∈ 𝐵) |
99 | 98 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐺 ↾ 𝑒)) ∈ 𝐵) |
100 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) |
101 | | simpll 767 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝜑) |
102 | | gsumle.c |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∘r ≤ 𝐺) |
103 | 102 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝐹 ∘r ≤ 𝐺) |
104 | 82 | ffnd 6505 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 Fn 𝐴) |
105 | 67 | ffnd 6505 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 Fn 𝐴) |
106 | | inidm 4109 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
107 | | eqidd 2739 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
108 | | eqidd 2739 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) = (𝐺‘𝑦)) |
109 | 104, 105,
1, 1, 106, 107, 108 | ofrval 7436 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐹 ∘r ≤ 𝐺 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ≤ (𝐺‘𝑦)) |
110 | 101, 103,
75, 109 | syl3anc 1372 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐹‘𝑦) ≤ (𝐺‘𝑦)) |
111 | 110 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝐹‘𝑦) ≤ (𝐺‘𝑦)) |
112 | 79 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → 𝑀 ∈ CMnd) |
113 | 45, 49, 65, 66, 77, 91, 93, 99, 100, 111, 112 | omndadd2d 30911 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → ((𝑀 Σg (𝐹 ↾ 𝑒))(+g‘𝑀)(𝐹‘𝑦)) ≤ ((𝑀 Σg (𝐺 ↾ 𝑒))(+g‘𝑀)(𝐺‘𝑦))) |
114 | 96 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → 𝑒 ∈ Fin) |
115 | 82 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 ∈ 𝑒) → 𝐹:𝐴⟶𝐵) |
116 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 ∈ 𝑒) → (𝑒 ∪ {𝑦}) ⊆ 𝐴) |
117 | | elun1 4066 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑒 → 𝑧 ∈ (𝑒 ∪ {𝑦})) |
118 | 117 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 ∈ 𝑒) → 𝑧 ∈ (𝑒 ∪ {𝑦})) |
119 | 116, 118 | sseldd 3878 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 ∈ 𝑒) → 𝑧 ∈ 𝐴) |
120 | 115, 119 | ffvelrnd 6862 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 ∈ 𝑒) → (𝐹‘𝑧) ∈ 𝐵) |
121 | 120 | ex 416 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑧 ∈ 𝑒 → (𝐹‘𝑧) ∈ 𝐵)) |
122 | 121 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑧 ∈ 𝑒 → (𝐹‘𝑧) ∈ 𝐵)) |
123 | 122 | imp 410 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) ∧ 𝑧 ∈ 𝑒) → (𝐹‘𝑧) ∈ 𝐵) |
124 | 71 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → 𝑦 ∈ V) |
125 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → ¬ 𝑦 ∈ 𝑒) |
126 | | fveq2 6674 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦)) |
127 | 45, 65, 112, 114, 123, 124, 125, 93, 126 | gsumunsn 19199 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹‘𝑧))) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐹‘𝑧)))(+g‘𝑀)(𝐹‘𝑦))) |
128 | 83, 69 | feqresmpt 6738 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐹 ↾ (𝑒 ∪ {𝑦})) = (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹‘𝑧))) |
129 | 128 | oveq2d 7186 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹‘𝑧)))) |
130 | 83, 84 | feqresmpt 6738 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐹 ↾ 𝑒) = (𝑧 ∈ 𝑒 ↦ (𝐹‘𝑧))) |
131 | 130 | oveq2d 7186 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐹 ↾ 𝑒)) = (𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐹‘𝑧)))) |
132 | 131 | oveq1d 7185 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → ((𝑀 Σg (𝐹 ↾ 𝑒))(+g‘𝑀)(𝐹‘𝑦)) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐹‘𝑧)))(+g‘𝑀)(𝐹‘𝑦))) |
133 | 129, 132 | eqeq12d 2754 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → ((𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹 ↾ 𝑒))(+g‘𝑀)(𝐹‘𝑦)) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹‘𝑧))) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐹‘𝑧)))(+g‘𝑀)(𝐹‘𝑦)))) |
134 | 133 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → ((𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹 ↾ 𝑒))(+g‘𝑀)(𝐹‘𝑦)) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹‘𝑧))) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐹‘𝑧)))(+g‘𝑀)(𝐹‘𝑦)))) |
135 | 127, 134 | mpbird 260 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹 ↾ 𝑒))(+g‘𝑀)(𝐹‘𝑦))) |
136 | 67 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝐺:𝐴⟶𝐵) |
137 | 136 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ 𝑧 ∈ 𝑒) → 𝐺:𝐴⟶𝐵) |
138 | 119 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ 𝑧 ∈ 𝑒) → 𝑧 ∈ 𝐴) |
139 | 137, 138 | ffvelrnd 6862 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ 𝑧 ∈ 𝑒) → (𝐺‘𝑧) ∈ 𝐵) |
140 | 71 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑦 ∈ V) |
141 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → ¬ 𝑦 ∈ 𝑒) |
142 | | fveq2 6674 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑦 → (𝐺‘𝑧) = (𝐺‘𝑦)) |
143 | 45, 65, 79, 96, 139, 140, 141, 76, 142 | gsumunsn 19199 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺‘𝑧))) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐺‘𝑧)))(+g‘𝑀)(𝐺‘𝑦))) |
144 | | simpr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑒 ∪ {𝑦}) ⊆ 𝐴) |
145 | 136, 144 | feqresmpt 6738 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺 ↾ (𝑒 ∪ {𝑦})) = (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺‘𝑧))) |
146 | 145 | oveq2d 7186 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺‘𝑧)))) |
147 | | resabs1 5855 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 ⊆ (𝑒 ∪ {𝑦}) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺 ↾ 𝑒)) |
148 | 57, 147 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺 ↾ 𝑒)) |
149 | 59 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑒 ⊆ 𝐴) |
150 | 136, 149 | feqresmpt 6738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺 ↾ 𝑒) = (𝑧 ∈ 𝑒 ↦ (𝐺‘𝑧))) |
151 | 148, 150 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝑧 ∈ 𝑒 ↦ (𝐺‘𝑧))) |
152 | 151 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒)) = (𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐺‘𝑧)))) |
153 | | resabs1 5855 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({𝑦} ⊆ (𝑒 ∪ {𝑦}) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦})) |
154 | 70, 153 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦})) |
155 | 70, 144 | sstrid 3888 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → {𝑦} ⊆ 𝐴) |
156 | 136, 155 | feqresmpt 6738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺 ↾ {𝑦}) = (𝑧 ∈ {𝑦} ↦ (𝐺‘𝑧))) |
157 | 154, 156 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝑧 ∈ {𝑦} ↦ (𝐺‘𝑧))) |
158 | 157 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝑀 Σg (𝑧 ∈ {𝑦} ↦ (𝐺‘𝑧)))) |
159 | 35, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 ∈ Mnd) |
160 | 159 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑀 ∈ Mnd) |
161 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦 ∈ V) |
162 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦 ∈ (𝑒 ∪ {𝑦})) |
163 | 144, 162 | sseldd 3878 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦 ∈ 𝐴) |
164 | 136, 163 | ffvelrnd 6862 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺‘𝑦) ∈ 𝐵) |
165 | 142 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 = 𝑦) → (𝐺‘𝑧) = (𝐺‘𝑦)) |
166 | 45, 160, 161, 164, 165 | gsumsnd 19191 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝑧 ∈ {𝑦} ↦ (𝐺‘𝑧))) = (𝐺‘𝑦)) |
167 | 158, 166 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝐺‘𝑦)) |
168 | 152, 167 | oveq12d 7188 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g‘𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐺‘𝑧)))(+g‘𝑀)(𝐺‘𝑦))) |
169 | 146, 168 | eqeq12d 2754 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g‘𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺‘𝑧))) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐺‘𝑧)))(+g‘𝑀)(𝐺‘𝑦)))) |
170 | 169 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → ((𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g‘𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺‘𝑧))) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐺‘𝑧)))(+g‘𝑀)(𝐺‘𝑦)))) |
171 | 143, 170 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g‘𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})))) |
172 | 57, 147 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺 ↾ 𝑒) |
173 | 172 | oveq2i 7181 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 Σg
((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒)) = (𝑀 Σg (𝐺 ↾ 𝑒)) |
174 | 70, 153 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦}) |
175 | 174 | oveq2i 7181 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 Σg
((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝑀 Σg (𝐺 ↾ {𝑦})) |
176 | 173, 175 | oveq12i 7182 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 Σg
((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g‘𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) = ((𝑀 Σg (𝐺 ↾ 𝑒))(+g‘𝑀)(𝑀 Σg (𝐺 ↾ {𝑦}))) |
177 | 171, 176 | eqtrdi 2789 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺 ↾ 𝑒))(+g‘𝑀)(𝑀 Σg (𝐺 ↾ {𝑦})))) |
178 | 70, 69 | sstrid 3888 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → {𝑦} ⊆ 𝐴) |
179 | 68, 178 | feqresmpt 6738 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐺 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ (𝐺‘𝑥))) |
180 | 179 | oveq2d 7186 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐺 ↾ {𝑦})) = (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺‘𝑥)))) |
181 | | cmnmnd 19040 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ CMnd → 𝑀 ∈ Mnd) |
182 | 79, 181 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑀 ∈ Mnd) |
183 | | fveq2 6674 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (𝐺‘𝑥) = (𝐺‘𝑦)) |
184 | 45, 183 | gsumsn 19193 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ Mnd ∧ 𝑦 ∈ V ∧ (𝐺‘𝑦) ∈ 𝐵) → (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺‘𝑥))) = (𝐺‘𝑦)) |
185 | 182, 140,
76, 184 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺‘𝑥))) = (𝐺‘𝑦)) |
186 | 180, 185 | eqtrd 2773 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐺 ↾ {𝑦})) = (𝐺‘𝑦)) |
187 | 186 | oveq2d 7186 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → ((𝑀 Σg (𝐺 ↾ 𝑒))(+g‘𝑀)(𝑀 Σg (𝐺 ↾ {𝑦}))) = ((𝑀 Σg (𝐺 ↾ 𝑒))(+g‘𝑀)(𝐺‘𝑦))) |
188 | 177, 187 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺 ↾ 𝑒))(+g‘𝑀)(𝐺‘𝑦))) |
189 | 188 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺 ↾ 𝑒))(+g‘𝑀)(𝐺‘𝑦))) |
190 | 113, 135,
189 | 3brtr4d 5062 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) ≤ (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))) |
191 | 62, 63, 64, 190 | syl21anc 837 |
. . . . . . . . 9
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) ≤ (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))) |
192 | 191 | exp31 423 |
. . . . . . . 8
⊢ ((𝑒 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑒) → ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒)) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) ≤ (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))))) |
193 | 192 | a2d 29 |
. . . . . . 7
⊢ ((𝑒 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑒) → (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) ≤ (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))))) |
194 | 61, 193 | syl5 34 |
. . . . . 6
⊢ ((𝑒 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑒) → (((𝜑 ∧ 𝑒 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) ≤ (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))))) |
195 | 10, 18, 26, 34, 56, 194 | findcard2s 8764 |
. . . . 5
⊢ (𝐴 ∈ Fin → ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝐴)) ≤ (𝑀 Σg (𝐺 ↾ 𝐴)))) |
196 | 195 | imp 410 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝜑 ∧ 𝐴 ⊆ 𝐴)) → (𝑀 Σg (𝐹 ↾ 𝐴)) ≤ (𝑀 Σg (𝐺 ↾ 𝐴))) |
197 | 2, 196 | mpanr2 704 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝜑) → (𝑀 Σg (𝐹 ↾ 𝐴)) ≤ (𝑀 Σg (𝐺 ↾ 𝐴))) |
198 | 1, 197 | mpancom 688 |
. 2
⊢ (𝜑 → (𝑀 Σg (𝐹 ↾ 𝐴)) ≤ (𝑀 Σg (𝐺 ↾ 𝐴))) |
199 | | fnresdm 6455 |
. . . 4
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
200 | 104, 199 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹 ↾ 𝐴) = 𝐹) |
201 | 200 | oveq2d 7186 |
. 2
⊢ (𝜑 → (𝑀 Σg (𝐹 ↾ 𝐴)) = (𝑀 Σg 𝐹)) |
202 | | fnresdm 6455 |
. . . 4
⊢ (𝐺 Fn 𝐴 → (𝐺 ↾ 𝐴) = 𝐺) |
203 | 105, 202 | syl 17 |
. . 3
⊢ (𝜑 → (𝐺 ↾ 𝐴) = 𝐺) |
204 | 203 | oveq2d 7186 |
. 2
⊢ (𝜑 → (𝑀 Σg (𝐺 ↾ 𝐴)) = (𝑀 Σg 𝐺)) |
205 | 198, 201,
204 | 3brtr3d 5061 |
1
⊢ (𝜑 → (𝑀 Σg 𝐹) ≤ (𝑀 Σg 𝐺)) |