| Step | Hyp | Ref
| Expression |
| 1 | | unieq 4918 |
. . . . 5
⊢ (𝑎 = ∅ → ∪ 𝑎 =
∪ ∅) |
| 2 | 1 | ineq2d 4220 |
. . . 4
⊢ (𝑎 = ∅ → (𝐸 ∩ ∪ 𝑎) =
(𝐸 ∩ ∪ ∅)) |
| 3 | 2 | fveq2d 6910 |
. . 3
⊢ (𝑎 = ∅ → (𝑀‘(𝐸 ∩ ∪ 𝑎)) = (𝑀‘(𝐸 ∩ ∪
∅))) |
| 4 | | esumeq1 34035 |
. . 3
⊢ (𝑎 = ∅ →
Σ*𝑦 ∈
𝑎(𝑀‘(𝐸 ∩ 𝑦)) = Σ*𝑦 ∈ ∅(𝑀‘(𝐸 ∩ 𝑦))) |
| 5 | 3, 4 | eqeq12d 2753 |
. 2
⊢ (𝑎 = ∅ → ((𝑀‘(𝐸 ∩ ∪ 𝑎)) = Σ*𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) ↔ (𝑀‘(𝐸 ∩ ∪
∅)) = Σ*𝑦 ∈ ∅(𝑀‘(𝐸 ∩ 𝑦)))) |
| 6 | | unieq 4918 |
. . . . 5
⊢ (𝑎 = 𝑏 → ∪ 𝑎 = ∪
𝑏) |
| 7 | 6 | ineq2d 4220 |
. . . 4
⊢ (𝑎 = 𝑏 → (𝐸 ∩ ∪ 𝑎) = (𝐸 ∩ ∪ 𝑏)) |
| 8 | 7 | fveq2d 6910 |
. . 3
⊢ (𝑎 = 𝑏 → (𝑀‘(𝐸 ∩ ∪ 𝑎)) = (𝑀‘(𝐸 ∩ ∪ 𝑏))) |
| 9 | | esumeq1 34035 |
. . 3
⊢ (𝑎 = 𝑏 → Σ*𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) = Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) |
| 10 | 8, 9 | eqeq12d 2753 |
. 2
⊢ (𝑎 = 𝑏 → ((𝑀‘(𝐸 ∩ ∪ 𝑎)) = Σ*𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) ↔ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)))) |
| 11 | | unieq 4918 |
. . . . 5
⊢ (𝑎 = (𝑏 ∪ {𝑥}) → ∪ 𝑎 = ∪
(𝑏 ∪ {𝑥})) |
| 12 | 11 | ineq2d 4220 |
. . . 4
⊢ (𝑎 = (𝑏 ∪ {𝑥}) → (𝐸 ∩ ∪ 𝑎) = (𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) |
| 13 | 12 | fveq2d 6910 |
. . 3
⊢ (𝑎 = (𝑏 ∪ {𝑥}) → (𝑀‘(𝐸 ∩ ∪ 𝑎)) = (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥})))) |
| 14 | | esumeq1 34035 |
. . 3
⊢ (𝑎 = (𝑏 ∪ {𝑥}) → Σ*𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) = Σ*𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦))) |
| 15 | 13, 14 | eqeq12d 2753 |
. 2
⊢ (𝑎 = (𝑏 ∪ {𝑥}) → ((𝑀‘(𝐸 ∩ ∪ 𝑎)) = Σ*𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) ↔ (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = Σ*𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦)))) |
| 16 | | unieq 4918 |
. . . . 5
⊢ (𝑎 = 𝐴 → ∪ 𝑎 = ∪
𝐴) |
| 17 | 16 | ineq2d 4220 |
. . . 4
⊢ (𝑎 = 𝐴 → (𝐸 ∩ ∪ 𝑎) = (𝐸 ∩ ∪ 𝐴)) |
| 18 | 17 | fveq2d 6910 |
. . 3
⊢ (𝑎 = 𝐴 → (𝑀‘(𝐸 ∩ ∪ 𝑎)) = (𝑀‘(𝐸 ∩ ∪ 𝐴))) |
| 19 | | esumeq1 34035 |
. . 3
⊢ (𝑎 = 𝐴 → Σ*𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) = Σ*𝑦 ∈ 𝐴(𝑀‘(𝐸 ∩ 𝑦))) |
| 20 | 18, 19 | eqeq12d 2753 |
. 2
⊢ (𝑎 = 𝐴 → ((𝑀‘(𝐸 ∩ ∪ 𝑎)) = Σ*𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) ↔ (𝑀‘(𝐸 ∩ ∪ 𝐴)) = Σ*𝑦 ∈ 𝐴(𝑀‘(𝐸 ∩ 𝑦)))) |
| 21 | | carsgsiga.1 |
. . 3
⊢ (𝜑 → (𝑀‘∅) = 0) |
| 22 | | uni0 4935 |
. . . . . 6
⊢ ∪ ∅ = ∅ |
| 23 | 22 | ineq2i 4217 |
. . . . 5
⊢ (𝐸 ∩ ∪ ∅) = (𝐸 ∩ ∅) |
| 24 | | in0 4395 |
. . . . 5
⊢ (𝐸 ∩ ∅) =
∅ |
| 25 | 23, 24 | eqtri 2765 |
. . . 4
⊢ (𝐸 ∩ ∪ ∅) = ∅ |
| 26 | 25 | fveq2i 6909 |
. . 3
⊢ (𝑀‘(𝐸 ∩ ∪
∅)) = (𝑀‘∅) |
| 27 | | esumnul 34049 |
. . 3
⊢
Σ*𝑦
∈ ∅(𝑀‘(𝐸 ∩ 𝑦)) = 0 |
| 28 | 21, 26, 27 | 3eqtr4g 2802 |
. 2
⊢ (𝜑 → (𝑀‘(𝐸 ∩ ∪
∅)) = Σ*𝑦 ∈ ∅(𝑀‘(𝐸 ∩ 𝑦))) |
| 29 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) |
| 30 | 29 | eqcomd 2743 |
. . . . 5
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) = (𝑀‘(𝐸 ∩ ∪ 𝑏))) |
| 31 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
| 32 | 31 | ineq2d 4220 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 = 𝑥) → (𝐸 ∩ 𝑦) = (𝐸 ∩ 𝑥)) |
| 33 | 32 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 = 𝑥) → (𝑀‘(𝐸 ∩ 𝑦)) = (𝑀‘(𝐸 ∩ 𝑥))) |
| 34 | | simprr 773 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝑥 ∈ (𝐴 ∖ 𝑏)) |
| 35 | | carsgval.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
| 36 | 35 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
| 37 | | carsgclctunlem1.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑂) |
| 38 | 37 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝐸 ∈ 𝒫 𝑂) |
| 39 | 38 | elpwincl1 32544 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝐸 ∩ 𝑥) ∈ 𝒫 𝑂) |
| 40 | 36, 39 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑀‘(𝐸 ∩ 𝑥)) ∈ (0[,]+∞)) |
| 41 | 33, 34, 40 | esumsn 34066 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → Σ*𝑦 ∈ {𝑥} (𝑀‘(𝐸 ∩ 𝑦)) = (𝑀‘(𝐸 ∩ 𝑥))) |
| 42 | 41 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → Σ*𝑦 ∈ {𝑥} (𝑀‘(𝐸 ∩ 𝑦)) = (𝑀‘(𝐸 ∩ 𝑥))) |
| 43 | 30, 42 | oveq12d 7449 |
. . . 4
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → (Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) +𝑒
Σ*𝑦 ∈
{𝑥} (𝑀‘(𝐸 ∩ 𝑦))) = ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +𝑒 (𝑀‘(𝐸 ∩ 𝑥)))) |
| 44 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑦(𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) |
| 45 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑦𝑏 |
| 46 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑦{𝑥} |
| 47 | | vex 3484 |
. . . . . . 7
⊢ 𝑏 ∈ V |
| 48 | 47 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝑏 ∈ V) |
| 49 | | vsnex 5434 |
. . . . . . 7
⊢ {𝑥} ∈ V |
| 50 | 49 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → {𝑥} ∈ V) |
| 51 | 34 | eldifbd 3964 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ¬ 𝑥 ∈ 𝑏) |
| 52 | | disjsn 4711 |
. . . . . . 7
⊢ ((𝑏 ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ 𝑏) |
| 53 | 51, 52 | sylibr 234 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑏 ∩ {𝑥}) = ∅) |
| 54 | 35 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ 𝑏) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
| 55 | 37 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ 𝑏) → 𝐸 ∈ 𝒫 𝑂) |
| 56 | 55 | elpwincl1 32544 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ 𝑏) → (𝐸 ∩ 𝑦) ∈ 𝒫 𝑂) |
| 57 | 54, 56 | ffvelcdmd 7105 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ 𝑏) → (𝑀‘(𝐸 ∩ 𝑦)) ∈ (0[,]+∞)) |
| 58 | 35 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ {𝑥}) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
| 59 | 37 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ {𝑥}) → 𝐸 ∈ 𝒫 𝑂) |
| 60 | 59 | elpwincl1 32544 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ {𝑥}) → (𝐸 ∩ 𝑦) ∈ 𝒫 𝑂) |
| 61 | 58, 60 | ffvelcdmd 7105 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ {𝑥}) → (𝑀‘(𝐸 ∩ 𝑦)) ∈ (0[,]+∞)) |
| 62 | 44, 45, 46, 48, 50, 53, 57, 61 | esumsplit 34054 |
. . . . 5
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → Σ*𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦)) = (Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) +𝑒
Σ*𝑦 ∈
{𝑥} (𝑀‘(𝐸 ∩ 𝑦)))) |
| 63 | 62 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → Σ*𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦)) = (Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) +𝑒
Σ*𝑦 ∈
{𝑥} (𝑀‘(𝐸 ∩ 𝑦)))) |
| 64 | | uniun 4930 |
. . . . . . . 8
⊢ ∪ (𝑏
∪ {𝑥}) = (∪ 𝑏
∪ ∪ {𝑥}) |
| 65 | | unisnv 4927 |
. . . . . . . . 9
⊢ ∪ {𝑥}
= 𝑥 |
| 66 | 65 | uneq2i 4165 |
. . . . . . . 8
⊢ (∪ 𝑏
∪ ∪ {𝑥}) = (∪ 𝑏 ∪ 𝑥) |
| 67 | 64, 66 | eqtri 2765 |
. . . . . . 7
⊢ ∪ (𝑏
∪ {𝑥}) = (∪ 𝑏
∪ 𝑥) |
| 68 | 67 | ineq2i 4217 |
. . . . . 6
⊢ (𝐸 ∩ ∪ (𝑏
∪ {𝑥})) = (𝐸 ∩ (∪ 𝑏
∪ 𝑥)) |
| 69 | 68 | fveq2i 6909 |
. . . . 5
⊢ (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) |
| 70 | | inass 4228 |
. . . . . . . . . 10
⊢ ((𝐸 ∩ (∪ 𝑏
∪ 𝑥)) ∩ ∪ 𝑏) =
(𝐸 ∩ ((∪ 𝑏
∪ 𝑥) ∩ ∪ 𝑏)) |
| 71 | | indir 4286 |
. . . . . . . . . . . 12
⊢ ((∪ 𝑏
∪ 𝑥) ∩ ∪ 𝑏) =
((∪ 𝑏 ∩ ∪ 𝑏) ∪ (𝑥 ∩ ∪ 𝑏)) |
| 72 | | inidm 4227 |
. . . . . . . . . . . . . . 15
⊢ (∪ 𝑏
∩ ∪ 𝑏) = ∪ 𝑏 |
| 73 | 72 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (∪
𝑏 ∩ ∪ 𝑏) =
∪ 𝑏) |
| 74 | | incom 4209 |
. . . . . . . . . . . . . . 15
⊢ (∪ 𝑏
∩ 𝑥) = (𝑥 ∩ ∪ 𝑏) |
| 75 | | carsgclctunlem1.1 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 𝑦) |
| 76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → Disj 𝑦 ∈ 𝐴 𝑦) |
| 77 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑏 ⊆ 𝐴) |
| 78 | 77 | adantrr 717 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝑏 ⊆ 𝐴) |
| 79 | 76, 78, 34 | disjuniel 32610 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (∪
𝑏 ∩ 𝑥) = ∅) |
| 80 | 74, 79 | eqtr3id 2791 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑥 ∩ ∪ 𝑏) = ∅) |
| 81 | 73, 80 | uneq12d 4169 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((∪
𝑏 ∩ ∪ 𝑏)
∪ (𝑥 ∩ ∪ 𝑏))
= (∪ 𝑏 ∪ ∅)) |
| 82 | | un0 4394 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑏
∪ ∅) = ∪ 𝑏 |
| 83 | 81, 82 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((∪
𝑏 ∩ ∪ 𝑏)
∪ (𝑥 ∩ ∪ 𝑏))
= ∪ 𝑏) |
| 84 | 71, 83 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((∪
𝑏 ∪ 𝑥) ∩ ∪ 𝑏) = ∪
𝑏) |
| 85 | 84 | ineq2d 4220 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝐸 ∩ ((∪ 𝑏 ∪ 𝑥) ∩ ∪ 𝑏)) = (𝐸 ∩ ∪ 𝑏)) |
| 86 | 70, 85 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏) = (𝐸 ∩ ∪ 𝑏)) |
| 87 | 86 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) = (𝑀‘(𝐸 ∩ ∪ 𝑏))) |
| 88 | | indif2 4281 |
. . . . . . . . . 10
⊢ (𝐸 ∩ ((∪ 𝑏
∪ 𝑥) ∖ ∪ 𝑏))
= ((𝐸 ∩ (∪ 𝑏
∪ 𝑥)) ∖ ∪ 𝑏) |
| 89 | | uncom 4158 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑏
∪ 𝑥) = (𝑥 ∪ ∪ 𝑏) |
| 90 | 89 | difeq1i 4122 |
. . . . . . . . . . . . 13
⊢ ((∪ 𝑏
∪ 𝑥) ∖ ∪ 𝑏) =
((𝑥 ∪ ∪ 𝑏)
∖ ∪ 𝑏) |
| 91 | | difun2 4481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∪ ∪ 𝑏)
∖ ∪ 𝑏) = (𝑥 ∖ ∪ 𝑏) |
| 92 | | disj3 4454 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∩ ∪ 𝑏) =
∅ ↔ 𝑥 = (𝑥 ∖ ∪ 𝑏)) |
| 93 | 92 | biimpi 216 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∩ ∪ 𝑏) =
∅ → 𝑥 = (𝑥 ∖ ∪ 𝑏)) |
| 94 | 91, 93 | eqtr4id 2796 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ ∪ 𝑏) =
∅ → ((𝑥 ∪
∪ 𝑏) ∖ ∪ 𝑏) = 𝑥) |
| 95 | 90, 94 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∩ ∪ 𝑏) =
∅ → ((∪ 𝑏 ∪ 𝑥) ∖ ∪ 𝑏) = 𝑥) |
| 96 | 80, 95 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((∪
𝑏 ∪ 𝑥) ∖ ∪ 𝑏) = 𝑥) |
| 97 | 96 | ineq2d 4220 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝐸 ∩ ((∪ 𝑏 ∪ 𝑥) ∖ ∪ 𝑏)) = (𝐸 ∩ 𝑥)) |
| 98 | 88, 97 | eqtr3id 2791 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏) = (𝐸 ∩ 𝑥)) |
| 99 | 98 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏)) = (𝑀‘(𝐸 ∩ 𝑥))) |
| 100 | 87, 99 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))) = ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +𝑒 (𝑀‘(𝐸 ∩ 𝑥)))) |
| 101 | | carsgval.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑂 ∈ 𝑉) |
| 102 | 101 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑂 ∈ 𝑉) |
| 103 | 35 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
| 104 | 21 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → (𝑀‘∅) = 0) |
| 105 | | carsgsiga.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
| 106 | 105 | 3adant1r 1178 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
| 107 | | fiunelcarsg.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ Fin) |
| 108 | | ssfi 9213 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑏 ⊆ 𝐴) → 𝑏 ∈ Fin) |
| 109 | 107, 108 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑏 ∈ Fin) |
| 110 | | fiunelcarsg.2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀)) |
| 111 | 110 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝐴 ⊆ (toCaraSiga‘𝑀)) |
| 112 | 77, 111 | sstrd 3994 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑏 ⊆ (toCaraSiga‘𝑀)) |
| 113 | 102, 103,
104, 106, 109, 112 | fiunelcarsg 34318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → ∪ 𝑏 ∈ (toCaraSiga‘𝑀)) |
| 114 | 101, 35 | elcarsg 34307 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∪ 𝑏
∈ (toCaraSiga‘𝑀)
↔ (∪ 𝑏 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒)))) |
| 115 | 114 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → (∪ 𝑏 ∈ (toCaraSiga‘𝑀) ↔ (∪ 𝑏
⊆ 𝑂 ∧
∀𝑒 ∈ 𝒫
𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒)))) |
| 116 | 113, 115 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → (∪ 𝑏 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒))) |
| 117 | 116 | simprd 495 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒)) |
| 118 | 117 | adantrr 717 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒)) |
| 119 | 38 | elpwincl1 32544 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∈ 𝒫 𝑂) |
| 120 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) |
| 121 | 120 | ineq1d 4219 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑒 ∩ ∪ 𝑏) = ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) |
| 122 | 121 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑀‘(𝑒 ∩ ∪ 𝑏)) = (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏))) |
| 123 | 120 | difeq1d 4125 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑒 ∖ ∪ 𝑏) = ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏)) |
| 124 | 123 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑀‘(𝑒 ∖ ∪ 𝑏)) = (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))) |
| 125 | 122, 124 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → ((𝑀‘(𝑒 ∩ ∪ 𝑏)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏)))) |
| 126 | 120 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑀‘𝑒) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥)))) |
| 127 | 125, 126 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (((𝑀‘(𝑒 ∩ ∪ 𝑏)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒) ↔ ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥))))) |
| 128 | 119, 127 | rspcdv 3614 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒) → ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥))))) |
| 129 | 118, 128 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥)))) |
| 130 | 100, 129 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +𝑒 (𝑀‘(𝐸 ∩ 𝑥))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥)))) |
| 131 | 130 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +𝑒 (𝑀‘(𝐸 ∩ 𝑥))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥)))) |
| 132 | 69, 131 | eqtr4id 2796 |
. . . 4
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +𝑒 (𝑀‘(𝐸 ∩ 𝑥)))) |
| 133 | 43, 63, 132 | 3eqtr4rd 2788 |
. . 3
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = Σ*𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦))) |
| 134 | 133 | ex 412 |
. 2
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) → (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = Σ*𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦)))) |
| 135 | 5, 10, 15, 20, 28, 134, 107 | findcard2d 9206 |
1
⊢ (𝜑 → (𝑀‘(𝐸 ∩ ∪ 𝐴)) = Σ*𝑦 ∈ 𝐴(𝑀‘(𝐸 ∩ 𝑦))) |