Step | Hyp | Ref
| Expression |
1 | | gsumle.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
2 | | ssid 3587 |
. . . 4
⊢ 𝐴 ⊆ 𝐴 |
3 | | sseq1 3589 |
. . . . . . . 8
⊢ (𝑎 = ∅ → (𝑎 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
4 | 3 | anbi2d 736 |
. . . . . . 7
⊢ (𝑎 = ∅ → ((𝜑 ∧ 𝑎 ⊆ 𝐴) ↔ (𝜑 ∧ ∅ ⊆ 𝐴))) |
5 | | reseq2 5312 |
. . . . . . . . 9
⊢ (𝑎 = ∅ → (𝐹 ↾ 𝑎) = (𝐹 ↾ ∅)) |
6 | 5 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑎 = ∅ → (𝑀 Σg
(𝐹 ↾ 𝑎)) = (𝑀 Σg (𝐹 ↾
∅))) |
7 | | reseq2 5312 |
. . . . . . . . 9
⊢ (𝑎 = ∅ → (𝐺 ↾ 𝑎) = (𝐺 ↾ ∅)) |
8 | 7 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑎 = ∅ → (𝑀 Σg
(𝐺 ↾ 𝑎)) = (𝑀 Σg (𝐺 ↾
∅))) |
9 | 6, 8 | breq12d 4596 |
. . . . . . 7
⊢ (𝑎 = ∅ → ((𝑀 Σg
(𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎)) ↔ (𝑀 Σg (𝐹 ↾ ∅)) ≤ (𝑀 Σg
(𝐺 ↾
∅)))) |
10 | 4, 9 | imbi12d 333 |
. . . . . 6
⊢ (𝑎 = ∅ → (((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎))) ↔ ((𝜑 ∧ ∅ ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ ∅)) ≤ (𝑀 Σg
(𝐺 ↾
∅))))) |
11 | | sseq1 3589 |
. . . . . . . 8
⊢ (𝑎 = 𝑒 → (𝑎 ⊆ 𝐴 ↔ 𝑒 ⊆ 𝐴)) |
12 | 11 | anbi2d 736 |
. . . . . . 7
⊢ (𝑎 = 𝑒 → ((𝜑 ∧ 𝑎 ⊆ 𝐴) ↔ (𝜑 ∧ 𝑒 ⊆ 𝐴))) |
13 | | reseq2 5312 |
. . . . . . . . 9
⊢ (𝑎 = 𝑒 → (𝐹 ↾ 𝑎) = (𝐹 ↾ 𝑒)) |
14 | 13 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑎 = 𝑒 → (𝑀 Σg (𝐹 ↾ 𝑎)) = (𝑀 Σg (𝐹 ↾ 𝑒))) |
15 | | reseq2 5312 |
. . . . . . . . 9
⊢ (𝑎 = 𝑒 → (𝐺 ↾ 𝑎) = (𝐺 ↾ 𝑒)) |
16 | 15 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑎 = 𝑒 → (𝑀 Σg (𝐺 ↾ 𝑎)) = (𝑀 Σg (𝐺 ↾ 𝑒))) |
17 | 14, 16 | breq12d 4596 |
. . . . . . 7
⊢ (𝑎 = 𝑒 → ((𝑀 Σg (𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎)) ↔ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒)))) |
18 | 12, 17 | imbi12d 333 |
. . . . . 6
⊢ (𝑎 = 𝑒 → (((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎))) ↔ ((𝜑 ∧ 𝑒 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))))) |
19 | | sseq1 3589 |
. . . . . . . 8
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → (𝑎 ⊆ 𝐴 ↔ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) |
20 | 19 | anbi2d 736 |
. . . . . . 7
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → ((𝜑 ∧ 𝑎 ⊆ 𝐴) ↔ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴))) |
21 | | reseq2 5312 |
. . . . . . . . 9
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → (𝐹 ↾ 𝑎) = (𝐹 ↾ (𝑒 ∪ {𝑦}))) |
22 | 21 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → (𝑀 Σg (𝐹 ↾ 𝑎)) = (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦})))) |
23 | | reseq2 5312 |
. . . . . . . . 9
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → (𝐺 ↾ 𝑎) = (𝐺 ↾ (𝑒 ∪ {𝑦}))) |
24 | 23 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → (𝑀 Σg (𝐺 ↾ 𝑎)) = (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))) |
25 | 22, 24 | breq12d 4596 |
. . . . . . 7
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → ((𝑀 Σg (𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎)) ↔ (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) ≤ (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))) |
26 | 20, 25 | imbi12d 333 |
. . . . . 6
⊢ (𝑎 = (𝑒 ∪ {𝑦}) → (((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎))) ↔ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) ≤ (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))))) |
27 | | sseq1 3589 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑎 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
28 | 27 | anbi2d 736 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝜑 ∧ 𝑎 ⊆ 𝐴) ↔ (𝜑 ∧ 𝐴 ⊆ 𝐴))) |
29 | | reseq2 5312 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (𝐹 ↾ 𝑎) = (𝐹 ↾ 𝐴)) |
30 | 29 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑀 Σg (𝐹 ↾ 𝑎)) = (𝑀 Σg (𝐹 ↾ 𝐴))) |
31 | | reseq2 5312 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (𝐺 ↾ 𝑎) = (𝐺 ↾ 𝐴)) |
32 | 31 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑀 Σg (𝐺 ↾ 𝑎)) = (𝑀 Σg (𝐺 ↾ 𝐴))) |
33 | 30, 32 | breq12d 4596 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝑀 Σg (𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎)) ↔ (𝑀 Σg (𝐹 ↾ 𝐴)) ≤ (𝑀 Σg (𝐺 ↾ 𝐴)))) |
34 | 28, 33 | imbi12d 333 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑎)) ≤ (𝑀 Σg (𝐺 ↾ 𝑎))) ↔ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝐴)) ≤ (𝑀 Σg (𝐺 ↾ 𝐴))))) |
35 | | gsumle.m |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ oMnd) |
36 | | omndtos 29036 |
. . . . . . . . . 10
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset) |
37 | | tospos 28989 |
. . . . . . . . . 10
⊢ (𝑀 ∈ Toset → 𝑀 ∈ Poset) |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ Poset) |
39 | | res0 5321 |
. . . . . . . . . . . 12
⊢ (𝐹 ↾ ∅) =
∅ |
40 | 39 | oveq2i 6560 |
. . . . . . . . . . 11
⊢ (𝑀 Σg
(𝐹 ↾ ∅)) =
(𝑀
Σg ∅) |
41 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(0g‘𝑀) = (0g‘𝑀) |
42 | 41 | gsum0 17101 |
. . . . . . . . . . 11
⊢ (𝑀 Σg
∅) = (0g‘𝑀) |
43 | 40, 42 | eqtri 2632 |
. . . . . . . . . 10
⊢ (𝑀 Σg
(𝐹 ↾ ∅)) =
(0g‘𝑀) |
44 | | omndmnd 29035 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Mnd) |
45 | | gsumle.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝑀) |
46 | 45, 41 | mndidcl 17131 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ Mnd →
(0g‘𝑀)
∈ 𝐵) |
47 | 35, 44, 46 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (0g‘𝑀) ∈ 𝐵) |
48 | 43, 47 | syl5eqel 2692 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) ∈ 𝐵) |
49 | | gsumle.l |
. . . . . . . . . 10
⊢ ≤ =
(le‘𝑀) |
50 | 45, 49 | posref 16774 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Poset ∧ (𝑀 Σg
(𝐹 ↾ ∅)) ∈
𝐵) → (𝑀 Σg
(𝐹 ↾ ∅)) ≤ (𝑀 Σg
(𝐹 ↾
∅))) |
51 | 38, 48, 50 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) ≤ (𝑀 Σg
(𝐹 ↾
∅))) |
52 | | res0 5321 |
. . . . . . . . . 10
⊢ (𝐺 ↾ ∅) =
∅ |
53 | 39, 52 | eqtr4i 2635 |
. . . . . . . . 9
⊢ (𝐹 ↾ ∅) = (𝐺 ↾
∅) |
54 | 53 | oveq2i 6560 |
. . . . . . . 8
⊢ (𝑀 Σg
(𝐹 ↾ ∅)) =
(𝑀
Σg (𝐺 ↾ ∅)) |
55 | 51, 54 | syl6breq 4624 |
. . . . . . 7
⊢ (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) ≤ (𝑀 Σg
(𝐺 ↾
∅))) |
56 | 55 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ∅ ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ ∅)) ≤ (𝑀 Σg
(𝐺 ↾
∅))) |
57 | | ssun1 3738 |
. . . . . . . . . 10
⊢ 𝑒 ⊆ (𝑒 ∪ {𝑦}) |
58 | | sstr2 3575 |
. . . . . . . . . 10
⊢ (𝑒 ⊆ (𝑒 ∪ {𝑦}) → ((𝑒 ∪ {𝑦}) ⊆ 𝐴 → 𝑒 ⊆ 𝐴)) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑒 ∪ {𝑦}) ⊆ 𝐴 → 𝑒 ⊆ 𝐴) |
60 | 59 | anim2i 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝜑 ∧ 𝑒 ⊆ 𝐴)) |
61 | 60 | imim1i 61 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒)))) |
62 | | simplr 788 |
. . . . . . . . . 10
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) |
63 | | simpllr 795 |
. . . . . . . . . 10
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → ¬ 𝑦 ∈ 𝑒) |
64 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) |
65 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(+g‘𝑀) = (+g‘𝑀) |
66 | 35 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → 𝑀 ∈ oMnd) |
67 | | gsumle.g |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺:𝐴⟶𝐵) |
68 | 67 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝐺:𝐴⟶𝐵) |
69 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑒 ∪ {𝑦}) ⊆ 𝐴) |
70 | | ssun2 3739 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑦} ⊆ (𝑒 ∪ {𝑦}) |
71 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V |
72 | 71 | snss 4259 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (𝑒 ∪ {𝑦}) ↔ {𝑦} ⊆ (𝑒 ∪ {𝑦})) |
73 | 70, 72 | mpbir 220 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ (𝑒 ∪ {𝑦}) |
74 | 73 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑦 ∈ (𝑒 ∪ {𝑦})) |
75 | 69, 74 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑦 ∈ 𝐴) |
76 | 68, 75 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐺‘𝑦) ∈ 𝐵) |
77 | 76 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝐺‘𝑦) ∈ 𝐵) |
78 | | gsumle.n |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ CMnd) |
79 | 78 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑀 ∈ CMnd) |
80 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑒 ∈ V |
81 | 80 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑒 ∈ V) |
82 | | gsumle.f |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
83 | 82 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝐹:𝐴⟶𝐵) |
84 | 57, 69 | syl5ss 3579 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑒 ⊆ 𝐴) |
85 | 83, 84 | fssresd 5984 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐹 ↾ 𝑒):𝑒⟶𝐵) |
86 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝐴 ∈ Fin) |
87 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢
(0g‘𝑀) ∈ V |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (0g‘𝑀) ∈ V) |
89 | 83, 86, 88 | fdmfifsupp 8168 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝐹 finSupp (0g‘𝑀)) |
90 | 89, 88 | fsuppres 8183 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐹 ↾ 𝑒) finSupp (0g‘𝑀)) |
91 | 45, 41, 79, 81, 85, 90 | gsumcl 18139 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐹 ↾ 𝑒)) ∈ 𝐵) |
92 | 91 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐹 ↾ 𝑒)) ∈ 𝐵) |
93 | 83, 75 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐹‘𝑦) ∈ 𝐵) |
94 | 93 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝐹‘𝑦) ∈ 𝐵) |
95 | 68, 84 | fssresd 5984 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐺 ↾ 𝑒):𝑒⟶𝐵) |
96 | | ssfi 8065 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ Fin ∧ 𝑒 ⊆ 𝐴) → 𝑒 ∈ Fin) |
97 | 86, 84, 96 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑒 ∈ Fin) |
98 | 95, 97, 88 | fdmfifsupp 8168 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐺 ↾ 𝑒) finSupp (0g‘𝑀)) |
99 | 45, 41, 79, 81, 95, 98 | gsumcl 18139 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐺 ↾ 𝑒)) ∈ 𝐵) |
100 | 99 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐺 ↾ 𝑒)) ∈ 𝐵) |
101 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) |
102 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝜑) |
103 | | gsumle.c |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∘𝑟 ≤ 𝐺) |
104 | 103 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝐹 ∘𝑟 ≤ 𝐺) |
105 | | ffn 5958 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
106 | 82, 105 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 Fn 𝐴) |
107 | | ffn 5958 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:𝐴⟶𝐵 → 𝐺 Fn 𝐴) |
108 | 67, 107 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 Fn 𝐴) |
109 | | inidm 3784 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
110 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
111 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) = (𝐺‘𝑦)) |
112 | 106, 108,
1, 1, 109, 110, 111 | ofrval 6805 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐹 ∘𝑟 ≤ 𝐺 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ≤ (𝐺‘𝑦)) |
113 | 102, 104,
75, 112 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐹‘𝑦) ≤ (𝐺‘𝑦)) |
114 | 113 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝐹‘𝑦) ≤ (𝐺‘𝑦)) |
115 | 79 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → 𝑀 ∈ CMnd) |
116 | 45, 49, 65, 66, 77, 92, 94, 100, 101, 114, 115 | omndadd2d 29039 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → ((𝑀 Σg (𝐹 ↾ 𝑒))(+g‘𝑀)(𝐹‘𝑦)) ≤ ((𝑀 Σg (𝐺 ↾ 𝑒))(+g‘𝑀)(𝐺‘𝑦))) |
117 | 97 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → 𝑒 ∈ Fin) |
118 | 82 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 ∈ 𝑒) → 𝐹:𝐴⟶𝐵) |
119 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 ∈ 𝑒) → (𝑒 ∪ {𝑦}) ⊆ 𝐴) |
120 | | elun1 3742 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑒 → 𝑧 ∈ (𝑒 ∪ {𝑦})) |
121 | 120 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 ∈ 𝑒) → 𝑧 ∈ (𝑒 ∪ {𝑦})) |
122 | 119, 121 | sseldd 3569 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 ∈ 𝑒) → 𝑧 ∈ 𝐴) |
123 | 118, 122 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 ∈ 𝑒) → (𝐹‘𝑧) ∈ 𝐵) |
124 | 123 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑧 ∈ 𝑒 → (𝐹‘𝑧) ∈ 𝐵)) |
125 | 124 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑧 ∈ 𝑒 → (𝐹‘𝑧) ∈ 𝐵)) |
126 | 125 | imp 444 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) ∧ 𝑧 ∈ 𝑒) → (𝐹‘𝑧) ∈ 𝐵) |
127 | 71 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → 𝑦 ∈ V) |
128 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → ¬ 𝑦 ∈ 𝑒) |
129 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦)) |
130 | 45, 65, 115, 117, 126, 127, 128, 94, 129 | gsumunsn 18182 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹‘𝑧))) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐹‘𝑧)))(+g‘𝑀)(𝐹‘𝑦))) |
131 | 83, 69 | feqresmpt 6160 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐹 ↾ (𝑒 ∪ {𝑦})) = (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹‘𝑧))) |
132 | 131 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹‘𝑧)))) |
133 | 83, 84 | feqresmpt 6160 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐹 ↾ 𝑒) = (𝑧 ∈ 𝑒 ↦ (𝐹‘𝑧))) |
134 | 133 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐹 ↾ 𝑒)) = (𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐹‘𝑧)))) |
135 | 134 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → ((𝑀 Σg (𝐹 ↾ 𝑒))(+g‘𝑀)(𝐹‘𝑦)) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐹‘𝑧)))(+g‘𝑀)(𝐹‘𝑦))) |
136 | 132, 135 | eqeq12d 2625 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → ((𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹 ↾ 𝑒))(+g‘𝑀)(𝐹‘𝑦)) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹‘𝑧))) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐹‘𝑧)))(+g‘𝑀)(𝐹‘𝑦)))) |
137 | 136 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → ((𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹 ↾ 𝑒))(+g‘𝑀)(𝐹‘𝑦)) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹‘𝑧))) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐹‘𝑧)))(+g‘𝑀)(𝐹‘𝑦)))) |
138 | 130, 137 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹 ↾ 𝑒))(+g‘𝑀)(𝐹‘𝑦))) |
139 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝐺:𝐴⟶𝐵) |
140 | 139 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ 𝑧 ∈ 𝑒) → 𝐺:𝐴⟶𝐵) |
141 | 122 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ 𝑧 ∈ 𝑒) → 𝑧 ∈ 𝐴) |
142 | 140, 141 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ 𝑧 ∈ 𝑒) → (𝐺‘𝑧) ∈ 𝐵) |
143 | 71 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑦 ∈ V) |
144 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → ¬ 𝑦 ∈ 𝑒) |
145 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑦 → (𝐺‘𝑧) = (𝐺‘𝑦)) |
146 | 45, 65, 79, 97, 142, 143, 144, 76, 145 | gsumunsn 18182 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺‘𝑧))) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐺‘𝑧)))(+g‘𝑀)(𝐺‘𝑦))) |
147 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑒 ∪ {𝑦}) ⊆ 𝐴) |
148 | 139, 147 | feqresmpt 6160 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺 ↾ (𝑒 ∪ {𝑦})) = (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺‘𝑧))) |
149 | 148 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺‘𝑧)))) |
150 | | resabs1 5347 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 ⊆ (𝑒 ∪ {𝑦}) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺 ↾ 𝑒)) |
151 | 57, 150 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺 ↾ 𝑒)) |
152 | 59 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑒 ⊆ 𝐴) |
153 | 139, 152 | feqresmpt 6160 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺 ↾ 𝑒) = (𝑧 ∈ 𝑒 ↦ (𝐺‘𝑧))) |
154 | 151, 153 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝑧 ∈ 𝑒 ↦ (𝐺‘𝑧))) |
155 | 154 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒)) = (𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐺‘𝑧)))) |
156 | | resabs1 5347 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({𝑦} ⊆ (𝑒 ∪ {𝑦}) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦})) |
157 | 70, 156 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦})) |
158 | 70, 147 | syl5ss 3579 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → {𝑦} ⊆ 𝐴) |
159 | 139, 158 | feqresmpt 6160 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺 ↾ {𝑦}) = (𝑧 ∈ {𝑦} ↦ (𝐺‘𝑧))) |
160 | 157, 159 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝑧 ∈ {𝑦} ↦ (𝐺‘𝑧))) |
161 | 160 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝑀 Σg (𝑧 ∈ {𝑦} ↦ (𝐺‘𝑧)))) |
162 | 35, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 ∈ Mnd) |
163 | 162 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑀 ∈ Mnd) |
164 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦 ∈ V) |
165 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦 ∈ (𝑒 ∪ {𝑦})) |
166 | 147, 165 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦 ∈ 𝐴) |
167 | 139, 166 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺‘𝑦) ∈ 𝐵) |
168 | 145 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 = 𝑦) → (𝐺‘𝑧) = (𝐺‘𝑦)) |
169 | 45, 163, 164, 167, 168 | gsumsnd 18175 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝑧 ∈ {𝑦} ↦ (𝐺‘𝑧))) = (𝐺‘𝑦)) |
170 | 161, 169 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝐺‘𝑦)) |
171 | 155, 170 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g‘𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐺‘𝑧)))(+g‘𝑀)(𝐺‘𝑦))) |
172 | 149, 171 | eqeq12d 2625 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g‘𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺‘𝑧))) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐺‘𝑧)))(+g‘𝑀)(𝐺‘𝑦)))) |
173 | 172 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → ((𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g‘𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺‘𝑧))) = ((𝑀 Σg (𝑧 ∈ 𝑒 ↦ (𝐺‘𝑧)))(+g‘𝑀)(𝐺‘𝑦)))) |
174 | 146, 173 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g‘𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})))) |
175 | 57, 150 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺 ↾ 𝑒) |
176 | 175 | oveq2i 6560 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 Σg
((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒)) = (𝑀 Σg (𝐺 ↾ 𝑒)) |
177 | 70, 156 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦}) |
178 | 177 | oveq2i 6560 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 Σg
((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝑀 Σg (𝐺 ↾ {𝑦})) |
179 | 176, 178 | oveq12i 6561 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 Σg
((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g‘𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) = ((𝑀 Σg (𝐺 ↾ 𝑒))(+g‘𝑀)(𝑀 Σg (𝐺 ↾ {𝑦}))) |
180 | 174, 179 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺 ↾ 𝑒))(+g‘𝑀)(𝑀 Σg (𝐺 ↾ {𝑦})))) |
181 | 70, 69 | syl5ss 3579 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → {𝑦} ⊆ 𝐴) |
182 | 68, 181 | feqresmpt 6160 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝐺 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ (𝐺‘𝑥))) |
183 | 182 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐺 ↾ {𝑦})) = (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺‘𝑥)))) |
184 | | cmnmnd 18031 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ CMnd → 𝑀 ∈ Mnd) |
185 | 79, 184 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → 𝑀 ∈ Mnd) |
186 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (𝐺‘𝑥) = (𝐺‘𝑦)) |
187 | 45, 186 | gsumsn 18177 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ Mnd ∧ 𝑦 ∈ V ∧ (𝐺‘𝑦) ∈ 𝐵) → (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺‘𝑥))) = (𝐺‘𝑦)) |
188 | 185, 143,
76, 187 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺‘𝑥))) = (𝐺‘𝑦)) |
189 | 183, 188 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐺 ↾ {𝑦})) = (𝐺‘𝑦)) |
190 | 189 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → ((𝑀 Σg (𝐺 ↾ 𝑒))(+g‘𝑀)(𝑀 Σg (𝐺 ↾ {𝑦}))) = ((𝑀 Σg (𝐺 ↾ 𝑒))(+g‘𝑀)(𝐺‘𝑦))) |
191 | 180, 190 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺 ↾ 𝑒))(+g‘𝑀)(𝐺‘𝑦))) |
192 | 191 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺 ↾ 𝑒))(+g‘𝑀)(𝐺‘𝑦))) |
193 | 116, 138,
192 | 3brtr4d 4615 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) ≤ (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))) |
194 | 62, 63, 64, 193 | syl21anc 1317 |
. . . . . . . . 9
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) ≤ (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))) |
195 | 194 | exp31 628 |
. . . . . . . 8
⊢ ((𝑒 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑒) → ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒)) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) ≤ (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))))) |
196 | 195 | a2d 29 |
. . . . . . 7
⊢ ((𝑒 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑒) → (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) ≤ (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))))) |
197 | 61, 196 | syl5 33 |
. . . . . 6
⊢ ((𝑒 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑒) → (((𝜑 ∧ 𝑒 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝑒)) ≤ (𝑀 Σg (𝐺 ↾ 𝑒))) → ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) ≤ (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))))) |
198 | 10, 18, 26, 34, 56, 197 | findcard2s 8086 |
. . . . 5
⊢ (𝐴 ∈ Fin → ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ 𝐴)) ≤ (𝑀 Σg (𝐺 ↾ 𝐴)))) |
199 | 198 | imp 444 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝜑 ∧ 𝐴 ⊆ 𝐴)) → (𝑀 Σg (𝐹 ↾ 𝐴)) ≤ (𝑀 Σg (𝐺 ↾ 𝐴))) |
200 | 2, 199 | mpanr2 716 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝜑) → (𝑀 Σg (𝐹 ↾ 𝐴)) ≤ (𝑀 Σg (𝐺 ↾ 𝐴))) |
201 | 1, 200 | mpancom 700 |
. 2
⊢ (𝜑 → (𝑀 Σg (𝐹 ↾ 𝐴)) ≤ (𝑀 Σg (𝐺 ↾ 𝐴))) |
202 | | fnresdm 5914 |
. . . 4
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
203 | 106, 202 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹 ↾ 𝐴) = 𝐹) |
204 | 203 | oveq2d 6565 |
. 2
⊢ (𝜑 → (𝑀 Σg (𝐹 ↾ 𝐴)) = (𝑀 Σg 𝐹)) |
205 | | fnresdm 5914 |
. . . 4
⊢ (𝐺 Fn 𝐴 → (𝐺 ↾ 𝐴) = 𝐺) |
206 | 108, 205 | syl 17 |
. . 3
⊢ (𝜑 → (𝐺 ↾ 𝐴) = 𝐺) |
207 | 206 | oveq2d 6565 |
. 2
⊢ (𝜑 → (𝑀 Σg (𝐺 ↾ 𝐴)) = (𝑀 Σg 𝐺)) |
208 | 201, 204,
207 | 3brtr3d 4614 |
1
⊢ (𝜑 → (𝑀 Σg 𝐹) ≤ (𝑀 Σg 𝐺)) |