measssd - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > measssd		Structured version Visualization version GIF version

Theorem measssd 30618

Description: A measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 28-Dec-2016.)

**Hypotheses**
Ref	Expression
measssd.1	⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))
measssd.2	⊢ (𝜑 → 𝐴 ∈ 𝑆)
measssd.3	⊢ (𝜑 → 𝐵 ∈ 𝑆)
measssd.4	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

**Assertion**
Ref	Expression
measssd	⊢ (𝜑 → (𝑀‘𝐴) ≤ (𝑀‘𝐵))

Proof of Theorem measssd Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		measssd.1	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))
2		measbase 30600	. . . . . . 7 ⊢ (𝑀 ∈ (measures‘𝑆) → 𝑆 ∈ ∪ ran sigAlgebra)
3	1, 2	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)
4		measssd.3	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
5		measssd.2	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
6		difelsiga 30536	. . . . . 6 ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → (𝐵 ∖ 𝐴) ∈ 𝑆)
7	3, 4, 5, 6	syl3anc 1476	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝐴) ∈ 𝑆)
8		measvxrge0 30608	. . . . 5 ⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝐵 ∖ 𝐴) ∈ 𝑆) → (𝑀‘(𝐵 ∖ 𝐴)) ∈ (0[,]+∞))
9	1, 7, 8	syl2anc 573	. . . 4 ⊢ (𝜑 → (𝑀‘(𝐵 ∖ 𝐴)) ∈ (0[,]+∞))
10		elxrge0 12488	. . . . 5 ⊢ ((𝑀‘(𝐵 ∖ 𝐴)) ∈ (0[,]+∞) ↔ ((𝑀‘(𝐵 ∖ 𝐴)) ∈ ℝ^* ∧ 0 ≤ (𝑀‘(𝐵 ∖ 𝐴))))
11	10	simprbi 484	. . . 4 ⊢ ((𝑀‘(𝐵 ∖ 𝐴)) ∈ (0[,]+∞) → 0 ≤ (𝑀‘(𝐵 ∖ 𝐴)))
12	9, 11	syl 17	. . 3 ⊢ (𝜑 → 0 ≤ (𝑀‘(𝐵 ∖ 𝐴)))
13		measvxrge0 30608	. . . . . 6 ⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑀‘𝐴) ∈ (0[,]+∞))
14	1, 5, 13	syl2anc 573	. . . . 5 ⊢ (𝜑 → (𝑀‘𝐴) ∈ (0[,]+∞))
15		elxrge0 12488	. . . . . 6 ⊢ ((𝑀‘𝐴) ∈ (0[,]+∞) ↔ ((𝑀‘𝐴) ∈ ℝ^* ∧ 0 ≤ (𝑀‘𝐴)))
16	15	simplbi 485	. . . . 5 ⊢ ((𝑀‘𝐴) ∈ (0[,]+∞) → (𝑀‘𝐴) ∈ ℝ^*)
17	14, 16	syl 17	. . . 4 ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ^*)
18	10	simplbi 485	. . . . 5 ⊢ ((𝑀‘(𝐵 ∖ 𝐴)) ∈ (0[,]+∞) → (𝑀‘(𝐵 ∖ 𝐴)) ∈ ℝ^*)
19	9, 18	syl 17	. . . 4 ⊢ (𝜑 → (𝑀‘(𝐵 ∖ 𝐴)) ∈ ℝ^*)
20		xraddge02 29861	. . . 4 ⊢ (((𝑀‘𝐴) ∈ ℝ^* ∧ (𝑀‘(𝐵 ∖ 𝐴)) ∈ ℝ^*) → (0 ≤ (𝑀‘(𝐵 ∖ 𝐴)) → (𝑀‘𝐴) ≤ ((𝑀‘𝐴) +_𝑒 (𝑀‘(𝐵 ∖ 𝐴)))))
21	17, 19, 20	syl2anc 573	. . 3 ⊢ (𝜑 → (0 ≤ (𝑀‘(𝐵 ∖ 𝐴)) → (𝑀‘𝐴) ≤ ((𝑀‘𝐴) +_𝑒 (𝑀‘(𝐵 ∖ 𝐴)))))
22	12, 21	mpd 15	. 2 ⊢ (𝜑 → (𝑀‘𝐴) ≤ ((𝑀‘𝐴) +_𝑒 (𝑀‘(𝐵 ∖ 𝐴))))
23		prssi 4488	. . . . . 6 ⊢ ((𝐴 ∈ 𝑆 ∧ (𝐵 ∖ 𝐴) ∈ 𝑆) → {𝐴, (𝐵 ∖ 𝐴)} ⊆ 𝑆)
24	5, 7, 23	syl2anc 573	. . . . 5 ⊢ (𝜑 → {𝐴, (𝐵 ∖ 𝐴)} ⊆ 𝑆)
25		prex 5038	. . . . . 6 ⊢ {𝐴, (𝐵 ∖ 𝐴)} ∈ V
26	25	elpw 4304	. . . . 5 ⊢ ({𝐴, (𝐵 ∖ 𝐴)} ∈ 𝒫 𝑆 ↔ {𝐴, (𝐵 ∖ 𝐴)} ⊆ 𝑆)
27	24, 26	sylibr 224	. . . 4 ⊢ (𝜑 → {𝐴, (𝐵 ∖ 𝐴)} ∈ 𝒫 𝑆)
28		prct 29832	. . . . 5 ⊢ ((𝐴 ∈ 𝑆 ∧ (𝐵 ∖ 𝐴) ∈ 𝑆) → {𝐴, (𝐵 ∖ 𝐴)} ≼ ω)
29	5, 7, 28	syl2anc 573	. . . 4 ⊢ (𝜑 → {𝐴, (𝐵 ∖ 𝐴)} ≼ ω)
30		disjdifprg 29726	. . . . . 6 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → Disj 𝑦 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑦)
31	5, 4, 30	syl2anc 573	. . . . 5 ⊢ (𝜑 → Disj 𝑦 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑦)
32		prcom 4404	. . . . . . 7 ⊢ {(𝐵 ∖ 𝐴), 𝐴} = {𝐴, (𝐵 ∖ 𝐴)}
33	32	a1i 11	. . . . . 6 ⊢ (𝜑 → {(𝐵 ∖ 𝐴), 𝐴} = {𝐴, (𝐵 ∖ 𝐴)})
34	33	disjeq1d 4763	. . . . 5 ⊢ (𝜑 → (Disj 𝑦 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑦 ↔ Disj 𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)}𝑦))
35	31, 34	mpbid 222	. . . 4 ⊢ (𝜑 → Disj 𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)}𝑦)
36		measvun 30612	. . . 4 ⊢ ((𝑀 ∈ (measures‘𝑆) ∧ {𝐴, (𝐵 ∖ 𝐴)} ∈ 𝒫 𝑆 ∧ ({𝐴, (𝐵 ∖ 𝐴)} ≼ ω ∧ Disj 𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)}𝑦)) → (𝑀‘∪ {𝐴, (𝐵 ∖ 𝐴)}) = Σ^*𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)} (𝑀‘𝑦))
37	1, 27, 29, 35, 36	syl112anc 1480	. . 3 ⊢ (𝜑 → (𝑀‘∪ {𝐴, (𝐵 ∖ 𝐴)}) = Σ^*𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)} (𝑀‘𝑦))
38		uniprg 4589	. . . . . 6 ⊢ ((𝐴 ∈ 𝑆 ∧ (𝐵 ∖ 𝐴) ∈ 𝑆) → ∪ {𝐴, (𝐵 ∖ 𝐴)} = (𝐴 ∪ (𝐵 ∖ 𝐴)))
39	5, 7, 38	syl2anc 573	. . . . 5 ⊢ (𝜑 → ∪ {𝐴, (𝐵 ∖ 𝐴)} = (𝐴 ∪ (𝐵 ∖ 𝐴)))
40		measssd.4	. . . . . 6 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
41		undif 4192	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)
42	40, 41	sylib 208	. . . . 5 ⊢ (𝜑 → (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)
43	39, 42	eqtrd 2805	. . . 4 ⊢ (𝜑 → ∪ {𝐴, (𝐵 ∖ 𝐴)} = 𝐵)
44	43	fveq2d 6337	. . 3 ⊢ (𝜑 → (𝑀‘∪ {𝐴, (𝐵 ∖ 𝐴)}) = (𝑀‘𝐵))
45		fveq2 6333	. . . . 5 ⊢ (𝑦 = 𝐴 → (𝑀‘𝑦) = (𝑀‘𝐴))
46	45	adantl 467	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = 𝐴) → (𝑀‘𝑦) = (𝑀‘𝐴))
47		fveq2 6333	. . . . 5 ⊢ (𝑦 = (𝐵 ∖ 𝐴) → (𝑀‘𝑦) = (𝑀‘(𝐵 ∖ 𝐴)))
48	47	adantl 467	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = (𝐵 ∖ 𝐴)) → (𝑀‘𝑦) = (𝑀‘(𝐵 ∖ 𝐴)))
49		eqimss 3806	. . . . . . . . . 10 ⊢ (𝐴 = (𝐵 ∖ 𝐴) → 𝐴 ⊆ (𝐵 ∖ 𝐴))
50		ssdifeq0 4194	. . . . . . . . . 10 ⊢ (𝐴 ⊆ (𝐵 ∖ 𝐴) ↔ 𝐴 = ∅)
51	49, 50	sylib 208	. . . . . . . . 9 ⊢ (𝐴 = (𝐵 ∖ 𝐴) → 𝐴 = ∅)
52	51	adantl 467	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐴 = (𝐵 ∖ 𝐴)) → 𝐴 = ∅)
53	52	fveq2d 6337	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐴 = (𝐵 ∖ 𝐴)) → (𝑀‘𝐴) = (𝑀‘∅))
54		measvnul 30609	. . . . . . . . 9 ⊢ (𝑀 ∈ (measures‘𝑆) → (𝑀‘∅) = 0)
55	1, 54	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘∅) = 0)
56	55	adantr 466	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐴 = (𝐵 ∖ 𝐴)) → (𝑀‘∅) = 0)
57	53, 56	eqtrd 2805	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 = (𝐵 ∖ 𝐴)) → (𝑀‘𝐴) = 0)
58	57	orcd 862	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 = (𝐵 ∖ 𝐴)) → ((𝑀‘𝐴) = 0 ∨ (𝑀‘𝐴) = +∞))
59	58	ex 397	. . . 4 ⊢ (𝜑 → (𝐴 = (𝐵 ∖ 𝐴) → ((𝑀‘𝐴) = 0 ∨ (𝑀‘𝐴) = +∞)))
60	46, 48, 5, 7, 14, 9, 59	esumpr2 30469	. . 3 ⊢ (𝜑 → Σ^*𝑦 ∈ {𝐴, (𝐵 ∖ 𝐴)} (𝑀‘𝑦) = ((𝑀‘𝐴) +_𝑒 (𝑀‘(𝐵 ∖ 𝐴))))
61	37, 44, 60	3eqtr3d 2813	. 2 ⊢ (𝜑 → (𝑀‘𝐵) = ((𝑀‘𝐴) +_𝑒 (𝑀‘(𝐵 ∖ 𝐴))))
62	22, 61	breqtrrd 4815	1 ⊢ (𝜑 → (𝑀‘𝐴) ≤ (𝑀‘𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 382 ∨ wo 836 = wceq 1631 ∈ wcel 2145 ∖ cdif 3720 ∪ cun 3721 ⊆ wss 3723 ∅c0 4063 𝒫 cpw 4298 {cpr 4319 ∪ cuni 4575 Disj wdisj 4755 class class class wbr 4787 ran crn 5251 ‘cfv 6030 (class class class)co 6796 ωcom 7216 ≼ cdom 8111 0cc0 10142 +∞cpnf 10277 ℝ^*cxr 10279 ≤ cle 10281 +_𝑒 cxad 12149 [,]cicc 12383 Σ^*cesum 30429 sigAlgebracsiga 30510 measurescmeas 30598

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4905 ax-sep 4916 ax-nul 4924 ax-pow 4975 ax-pr 5035 ax-un 7100 ax-inf2 8706 ax-ac2 9491 ax-cnex 10198 ax-resscn 10199 ax-1cn 10200 ax-icn 10201 ax-addcl 10202 ax-addrcl 10203 ax-mulcl 10204 ax-mulrcl 10205 ax-mulcom 10206 ax-addass 10207 ax-mulass 10208 ax-distr 10209 ax-i2m1 10210 ax-1ne0 10211 ax-1rid 10212 ax-rnegex 10213 ax-rrecex 10214 ax-cnre 10215 ax-pre-lttri 10216 ax-pre-lttrn 10217 ax-pre-ltadd 10218 ax-pre-mulgt0 10219 ax-pre-sup 10220 ax-addf 10221 ax-mulf 10222

This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-fal 1637 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-tp 4322 df-op 4324 df-uni 4576 df-int 4613 df-iun 4657 df-iin 4658 df-disj 4756 df-br 4788 df-opab 4848 df-mpt 4865 df-tr 4888 df-id 5158 df-eprel 5163 df-po 5171 df-so 5172 df-fr 5209 df-se 5210 df-we 5211 df-xp 5256 df-rel 5257 df-cnv 5258 df-co 5259 df-dm 5260 df-rn 5261 df-res 5262 df-ima 5263 df-pred 5822 df-ord 5868 df-on 5869 df-lim 5870 df-suc 5871 df-iota 5993 df-fun 6032 df-fn 6033 df-f 6034 df-f1 6035 df-fo 6036 df-f1o 6037 df-fv 6038 df-isom 6039 df-riota 6757 df-ov 6799 df-oprab 6800 df-mpt2 6801 df-of 7048 df-om 7217 df-1st 7319 df-2nd 7320 df-supp 7451 df-wrecs 7563 df-recs 7625 df-rdg 7663 df-1o 7717 df-2o 7718 df-oadd 7721 df-er 7900 df-map 8015 df-pm 8016 df-ixp 8067 df-en 8114 df-dom 8115 df-sdom 8116 df-fin 8117 df-fsupp 8436 df-fi 8477 df-sup 8508 df-inf 8509 df-oi 8575 df-card 8969 df-acn 8972 df-ac 9143 df-cda 9196 df-pnf 10282 df-mnf 10283 df-xr 10284 df-ltxr 10285 df-le 10286 df-sub 10474 df-neg 10475 df-div 10891 df-nn 11227 df-2 11285 df-3 11286 df-4 11287 df-5 11288 df-6 11289 df-7 11290 df-8 11291 df-9 11292 df-n0 11500 df-z 11585 df-dec 11701 df-uz 11894 df-q 11997 df-rp 12036 df-xneg 12151 df-xadd 12152 df-xmul 12153 df-ioo 12384 df-ioc 12385 df-ico 12386 df-icc 12387 df-fz 12534 df-fzo 12674 df-fl 12801 df-mod 12877 df-seq 13009 df-exp 13068 df-fac 13265 df-bc 13294 df-hash 13322 df-shft 14015 df-cj 14047 df-re 14048 df-im 14049 df-sqrt 14183 df-abs 14184 df-limsup 14410 df-clim 14427 df-rlim 14428 df-sum 14625 df-ef 15004 df-sin 15006 df-cos 15007 df-pi 15009 df-struct 16066 df-ndx 16067 df-slot 16068 df-base 16070 df-sets 16071 df-ress 16072 df-plusg 16162 df-mulr 16163 df-starv 16164 df-sca 16165 df-vsca 16166 df-ip 16167 df-tset 16168 df-ple 16169 df-ds 16172 df-unif 16173 df-hom 16174 df-cco 16175 df-rest 16291 df-topn 16292 df-0g 16310 df-gsum 16311 df-topgen 16312 df-pt 16313 df-prds 16316 df-ordt 16369 df-xrs 16370 df-qtop 16375 df-imas 16376 df-xps 16378 df-mre 16454 df-mrc 16455 df-acs 16457 df-ps 17408 df-tsr 17409 df-plusf 17449 df-mgm 17450 df-sgrp 17492 df-mnd 17503 df-mhm 17543 df-submnd 17544 df-grp 17633 df-minusg 17634 df-sbg 17635 df-mulg 17749 df-subg 17799 df-cntz 17957 df-cmn 18402 df-abl 18403 df-mgp 18698 df-ur 18710 df-ring 18757 df-cring 18758 df-subrg 18988 df-abv 19027 df-lmod 19075 df-scaf 19076 df-sra 19387 df-rgmod 19388 df-psmet 19953 df-xmet 19954 df-met 19955 df-bl 19956 df-mopn 19957 df-fbas 19958 df-fg 19959 df-cnfld 19962 df-top 20919 df-topon 20936 df-topsp 20958 df-bases 20971 df-cld 21044 df-ntr 21045 df-cls 21046 df-nei 21123 df-lp 21161 df-perf 21162 df-cn 21252 df-cnp 21253 df-haus 21340 df-tx 21586 df-hmeo 21779 df-fil 21870 df-fm 21962 df-flim 21963 df-flf 21964 df-tmd 22096 df-tgp 22097 df-tsms 22150 df-trg 22183 df-xms 22345 df-ms 22346 df-tms 22347 df-nm 22607 df-ngp 22608 df-nrg 22610 df-nlm 22611 df-ii 22900 df-cncf 22901 df-limc 23850 df-dv 23851 df-log 24524 df-esum 30430 df-siga 30511 df-meas 30599

This theorem is referenced by: measiun 30621 aean 30647 sibfinima 30741 prob01 30815 probinc 30823 probmeasb 30832 cndprob01 30837 dstfrvinc 30878

W3C validator