Proof of Theorem pmeasmono
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqimss 4041 | . . . . . . 7
⊢ (𝐴 = (𝐵 ∖ 𝐴) → 𝐴 ⊆ (𝐵 ∖ 𝐴)) | 
| 2 |  | ssdifeq0 4486 | . . . . . . 7
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐴) ↔ 𝐴 = ∅) | 
| 3 | 1, 2 | sylib 218 | . . . . . 6
⊢ (𝐴 = (𝐵 ∖ 𝐴) → 𝐴 = ∅) | 
| 4 | 3 | fveq2d 6909 | . . . . 5
⊢ (𝐴 = (𝐵 ∖ 𝐴) → (𝑃‘𝐴) = (𝑃‘∅)) | 
| 5 | 4 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝐴 = (𝐵 ∖ 𝐴)) → (𝑃‘𝐴) = (𝑃‘∅)) | 
| 6 |  | caraext.2 | . . . . 5
⊢ (𝜑 → (𝑃‘∅) = 0) | 
| 7 | 6 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 = (𝐵 ∖ 𝐴)) → (𝑃‘∅) = 0) | 
| 8 | 5, 7 | eqtrd 2776 | . . 3
⊢ ((𝜑 ∧ 𝐴 = (𝐵 ∖ 𝐴)) → (𝑃‘𝐴) = 0) | 
| 9 |  | caraext.1 | . . . . . 6
⊢ (𝜑 → 𝑃:𝑅⟶(0[,]+∞)) | 
| 10 |  | pmeasmono.2 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑅) | 
| 11 | 9, 10 | ffvelcdmd 7104 | . . . . 5
⊢ (𝜑 → (𝑃‘𝐵) ∈ (0[,]+∞)) | 
| 12 |  | elxrge0 13498 | . . . . . 6
⊢ ((𝑃‘𝐵) ∈ (0[,]+∞) ↔ ((𝑃‘𝐵) ∈ ℝ* ∧ 0 ≤
(𝑃‘𝐵))) | 
| 13 | 12 | simprbi 496 | . . . . 5
⊢ ((𝑃‘𝐵) ∈ (0[,]+∞) → 0 ≤ (𝑃‘𝐵)) | 
| 14 | 11, 13 | syl 17 | . . . 4
⊢ (𝜑 → 0 ≤ (𝑃‘𝐵)) | 
| 15 | 14 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝐴 = (𝐵 ∖ 𝐴)) → 0 ≤ (𝑃‘𝐵)) | 
| 16 | 8, 15 | eqbrtrd 5164 | . 2
⊢ ((𝜑 ∧ 𝐴 = (𝐵 ∖ 𝐴)) → (𝑃‘𝐴) ≤ (𝑃‘𝐵)) | 
| 17 |  | iccssxr 13471 | . . . . 5
⊢
(0[,]+∞) ⊆ ℝ* | 
| 18 | 9 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → 𝑃:𝑅⟶(0[,]+∞)) | 
| 19 |  | pmeasmono.1 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑅) | 
| 20 | 19 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → 𝐴 ∈ 𝑅) | 
| 21 | 18, 20 | ffvelcdmd 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → (𝑃‘𝐴) ∈ (0[,]+∞)) | 
| 22 | 17, 21 | sselid 3980 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → (𝑃‘𝐴) ∈
ℝ*) | 
| 23 |  | pmeasmono.3 | . . . . . 6
⊢ (𝜑 → (𝐵 ∖ 𝐴) ∈ 𝑅) | 
| 24 | 23 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → (𝐵 ∖ 𝐴) ∈ 𝑅) | 
| 25 | 18, 24 | ffvelcdmd 7104 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → (𝑃‘(𝐵 ∖ 𝐴)) ∈ (0[,]+∞)) | 
| 26 |  | xrge0addge 32762 | . . . 4
⊢ (((𝑃‘𝐴) ∈ ℝ* ∧ (𝑃‘(𝐵 ∖ 𝐴)) ∈ (0[,]+∞)) → (𝑃‘𝐴) ≤ ((𝑃‘𝐴) +𝑒 (𝑃‘(𝐵 ∖ 𝐴)))) | 
| 27 | 22, 25, 26 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → (𝑃‘𝐴) ≤ ((𝑃‘𝐴) +𝑒 (𝑃‘(𝐵 ∖ 𝐴)))) | 
| 28 |  | prct 32727 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑅 ∧ (𝐵 ∖ 𝐴) ∈ 𝑅) → {𝐴, (𝐵 ∖ 𝐴)} ≼ ω) | 
| 29 | 19, 23, 28 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → {𝐴, (𝐵 ∖ 𝐴)} ≼ ω) | 
| 30 | 29 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → {𝐴, (𝐵 ∖ 𝐴)} ≼ ω) | 
| 31 |  | prssi 4820 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑅 ∧ (𝐵 ∖ 𝐴) ∈ 𝑅) → {𝐴, (𝐵 ∖ 𝐴)} ⊆ 𝑅) | 
| 32 | 19, 23, 31 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → {𝐴, (𝐵 ∖ 𝐴)} ⊆ 𝑅) | 
| 33 | 32 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → {𝐴, (𝐵 ∖ 𝐴)} ⊆ 𝑅) | 
| 34 |  | disjdif 4471 | . . . . . . 7
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ | 
| 35 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → 𝐴 ≠ (𝐵 ∖ 𝐴)) | 
| 36 |  | id 22 | . . . . . . . . 9
⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴) | 
| 37 |  | id 22 | . . . . . . . . 9
⊢ (𝑦 = (𝐵 ∖ 𝐴) → 𝑦 = (𝐵 ∖ 𝐴)) | 
| 38 | 36, 37 | disjprg 5138 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑅 ∧ (𝐵 ∖ 𝐴) ∈ 𝑅 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → (Disj 𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)}𝑦 ↔ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅)) | 
| 39 | 20, 24, 35, 38 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → (Disj 𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)}𝑦 ↔ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅)) | 
| 40 | 34, 39 | mpbiri 258 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → Disj 𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)}𝑦) | 
| 41 | 30, 33, 40 | 3jca 1128 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → ({𝐴, (𝐵 ∖ 𝐴)} ≼ ω ∧ {𝐴, (𝐵 ∖ 𝐴)} ⊆ 𝑅 ∧ Disj 𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)}𝑦)) | 
| 42 |  | prex 5436 | . . . . . . 7
⊢ {𝐴, (𝐵 ∖ 𝐴)} ∈ V | 
| 43 |  | biidd 262 | . . . . . . . . . 10
⊢ (𝑥 = {𝐴, (𝐵 ∖ 𝐴)} → (𝜑 ↔ 𝜑)) | 
| 44 |  | breq1 5145 | . . . . . . . . . . 11
⊢ (𝑥 = {𝐴, (𝐵 ∖ 𝐴)} → (𝑥 ≼ ω ↔ {𝐴, (𝐵 ∖ 𝐴)} ≼ ω)) | 
| 45 |  | sseq1 4008 | . . . . . . . . . . 11
⊢ (𝑥 = {𝐴, (𝐵 ∖ 𝐴)} → (𝑥 ⊆ 𝑅 ↔ {𝐴, (𝐵 ∖ 𝐴)} ⊆ 𝑅)) | 
| 46 |  | disjeq1 5116 | . . . . . . . . . . 11
⊢ (𝑥 = {𝐴, (𝐵 ∖ 𝐴)} → (Disj 𝑦 ∈ 𝑥 𝑦 ↔ Disj 𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)}𝑦)) | 
| 47 | 44, 45, 46 | 3anbi123d 1437 | . . . . . . . . . 10
⊢ (𝑥 = {𝐴, (𝐵 ∖ 𝐴)} → ((𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦) ↔ ({𝐴, (𝐵 ∖ 𝐴)} ≼ ω ∧ {𝐴, (𝐵 ∖ 𝐴)} ⊆ 𝑅 ∧ Disj 𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)}𝑦))) | 
| 48 | 43, 47 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑥 = {𝐴, (𝐵 ∖ 𝐴)} → ((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ↔ (𝜑 ∧ ({𝐴, (𝐵 ∖ 𝐴)} ≼ ω ∧ {𝐴, (𝐵 ∖ 𝐴)} ⊆ 𝑅 ∧ Disj 𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)}𝑦)))) | 
| 49 |  | unieq 4917 | . . . . . . . . . . 11
⊢ (𝑥 = {𝐴, (𝐵 ∖ 𝐴)} → ∪ 𝑥 = ∪
{𝐴, (𝐵 ∖ 𝐴)}) | 
| 50 | 49 | fveq2d 6909 | . . . . . . . . . 10
⊢ (𝑥 = {𝐴, (𝐵 ∖ 𝐴)} → (𝑃‘∪ 𝑥) = (𝑃‘∪ {𝐴, (𝐵 ∖ 𝐴)})) | 
| 51 |  | esumeq1 34036 | . . . . . . . . . 10
⊢ (𝑥 = {𝐴, (𝐵 ∖ 𝐴)} → Σ*𝑦 ∈ 𝑥(𝑃‘𝑦) = Σ*𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)} (𝑃‘𝑦)) | 
| 52 | 50, 51 | eqeq12d 2752 | . . . . . . . . 9
⊢ (𝑥 = {𝐴, (𝐵 ∖ 𝐴)} → ((𝑃‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑃‘𝑦) ↔ (𝑃‘∪ {𝐴, (𝐵 ∖ 𝐴)}) = Σ*𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)} (𝑃‘𝑦))) | 
| 53 | 48, 52 | imbi12d 344 | . . . . . . . 8
⊢ (𝑥 = {𝐴, (𝐵 ∖ 𝐴)} → (((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑃‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑃‘𝑦)) ↔ ((𝜑 ∧ ({𝐴, (𝐵 ∖ 𝐴)} ≼ ω ∧ {𝐴, (𝐵 ∖ 𝐴)} ⊆ 𝑅 ∧ Disj 𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)}𝑦)) → (𝑃‘∪ {𝐴, (𝐵 ∖ 𝐴)}) = Σ*𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)} (𝑃‘𝑦)))) | 
| 54 |  | caraext.3 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑃‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑃‘𝑦)) | 
| 55 | 53, 54 | vtoclg 3553 | . . . . . . 7
⊢ ({𝐴, (𝐵 ∖ 𝐴)} ∈ V → ((𝜑 ∧ ({𝐴, (𝐵 ∖ 𝐴)} ≼ ω ∧ {𝐴, (𝐵 ∖ 𝐴)} ⊆ 𝑅 ∧ Disj 𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)}𝑦)) → (𝑃‘∪ {𝐴, (𝐵 ∖ 𝐴)}) = Σ*𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)} (𝑃‘𝑦))) | 
| 56 | 42, 55 | ax-mp 5 | . . . . . 6
⊢ ((𝜑 ∧ ({𝐴, (𝐵 ∖ 𝐴)} ≼ ω ∧ {𝐴, (𝐵 ∖ 𝐴)} ⊆ 𝑅 ∧ Disj 𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)}𝑦)) → (𝑃‘∪ {𝐴, (𝐵 ∖ 𝐴)}) = Σ*𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)} (𝑃‘𝑦)) | 
| 57 | 56 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) ∧ ({𝐴, (𝐵 ∖ 𝐴)} ≼ ω ∧ {𝐴, (𝐵 ∖ 𝐴)} ⊆ 𝑅 ∧ Disj 𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)}𝑦)) → (𝑃‘∪ {𝐴, (𝐵 ∖ 𝐴)}) = Σ*𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)} (𝑃‘𝑦)) | 
| 58 | 41, 57 | mpdan 687 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → (𝑃‘∪ {𝐴, (𝐵 ∖ 𝐴)}) = Σ*𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)} (𝑃‘𝑦)) | 
| 59 |  | uniprg 4922 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑅 ∧ (𝐵 ∖ 𝐴) ∈ 𝑅) → ∪ {𝐴, (𝐵 ∖ 𝐴)} = (𝐴 ∪ (𝐵 ∖ 𝐴))) | 
| 60 | 19, 23, 59 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ∪ {𝐴,
(𝐵 ∖ 𝐴)} = (𝐴 ∪ (𝐵 ∖ 𝐴))) | 
| 61 |  | pmeasmono.4 | . . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ 𝐵) | 
| 62 |  | undif 4481 | . . . . . . . 8
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵) | 
| 63 | 61, 62 | sylib 218 | . . . . . . 7
⊢ (𝜑 → (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵) | 
| 64 | 60, 63 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → ∪ {𝐴,
(𝐵 ∖ 𝐴)} = 𝐵) | 
| 65 | 64 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → ∪
{𝐴, (𝐵 ∖ 𝐴)} = 𝐵) | 
| 66 | 65 | fveq2d 6909 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → (𝑃‘∪ {𝐴, (𝐵 ∖ 𝐴)}) = (𝑃‘𝐵)) | 
| 67 |  | simpr 484 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) ∧ 𝑦 = 𝐴) → 𝑦 = 𝐴) | 
| 68 | 67 | fveq2d 6909 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) ∧ 𝑦 = 𝐴) → (𝑃‘𝑦) = (𝑃‘𝐴)) | 
| 69 |  | simpr 484 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) ∧ 𝑦 = (𝐵 ∖ 𝐴)) → 𝑦 = (𝐵 ∖ 𝐴)) | 
| 70 | 69 | fveq2d 6909 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) ∧ 𝑦 = (𝐵 ∖ 𝐴)) → (𝑃‘𝑦) = (𝑃‘(𝐵 ∖ 𝐴))) | 
| 71 | 68, 70, 20, 24, 21, 25, 35 | esumpr 34068 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → Σ*𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)} (𝑃‘𝑦) = ((𝑃‘𝐴) +𝑒 (𝑃‘(𝐵 ∖ 𝐴)))) | 
| 72 | 58, 66, 71 | 3eqtr3d 2784 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → (𝑃‘𝐵) = ((𝑃‘𝐴) +𝑒 (𝑃‘(𝐵 ∖ 𝐴)))) | 
| 73 | 27, 72 | breqtrrd 5170 | . 2
⊢ ((𝜑 ∧ 𝐴 ≠ (𝐵 ∖ 𝐴)) → (𝑃‘𝐴) ≤ (𝑃‘𝐵)) | 
| 74 | 16, 73 | pm2.61dane 3028 | 1
⊢ (𝜑 → (𝑃‘𝐴) ≤ (𝑃‘𝐵)) |