omsmon

Description: A constructed outer measure is monotone. Note in Example 1.5.2 of Bogachev p. 17. (Contributed by Thierry Arnoux, 15-Sep-2019) (Revised by AV, 4-Oct-2020)

	Ref	Expression
Hypotheses	oms.m	$⊢ M = toOMeas (R)$
	oms.o	$⊢ φ \to Q \in V$
	oms.r	$⊢ φ \to R : Q ⟶ [0, +∞]$
	omsmon.a	$⊢ φ \to A \subseteq B$
	omsmon.b	$⊢ φ \to B \subseteq ⋃ Q$
Assertion	omsmon	$⊢ φ \to M (A) \leq M (B)$

Proof

Step	Hyp	Ref	Expression
1		oms.m	$⊢ M = toOMeas (R)$
2		oms.o	$⊢ φ \to Q \in V$
3		oms.r	$⊢ φ \to R : Q ⟶ [0, +∞]$
4		omsmon.a	$⊢ φ \to A \subseteq B$
5		omsmon.b	$⊢ φ \to B \subseteq ⋃ Q$
6	4	adantr	$⊢ (φ \land z \in 𝒫 dom R) \to A \subseteq B$
7		sstr2	$⊢ A \subseteq B \to (B \subseteq ⋃ z \to A \subseteq ⋃ z)$
8	6 7	syl	$⊢ (φ \land z \in 𝒫 dom R) \to (B \subseteq ⋃ z \to A \subseteq ⋃ z)$
9	8	anim1d	$⊢ (φ \land z \in 𝒫 dom R) \to ((B \subseteq ⋃ z \land z ≼ ω) \to (A \subseteq ⋃ z \land z ≼ ω))$
10	9	ss2rabdv	$⊢ φ \to \{z \in 𝒫 dom R \| (B \subseteq ⋃ z \land z ≼ ω)\} \subseteq \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}$
11		resmpt	$⊢ \{z \in 𝒫 dom R \| (B \subseteq ⋃ z \land z ≼ ω)\} \subseteq \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \to {(x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) ↾}_{\{z \in 𝒫 dom R \| (B \subseteq ⋃ z \land z ≼ ω)\}} = (x \in \{z \in 𝒫 dom R \| (B \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))$
12	10 11	syl	$⊢ φ \to {(x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) ↾}_{\{z \in 𝒫 dom R \| (B \subseteq ⋃ z \land z ≼ ω)\}} = (x \in \{z \in 𝒫 dom R \| (B \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))$
13		resss	$⊢ {(x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) ↾}_{\{z \in 𝒫 dom R \| (B \subseteq ⋃ z \land z ≼ ω)\}} \subseteq (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))$
14	12 13	eqsstrrdi	$⊢ φ \to (x \in \{z \in 𝒫 dom R \| (B \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) \subseteq (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))$
15		rnss	$⊢ (x \in \{z \in 𝒫 dom R \| (B \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) \subseteq (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) \to ran (x \in \{z \in 𝒫 dom R \| (B \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) \subseteq ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))$
16	14 15	syl	$⊢ φ \to ran (x \in \{z \in 𝒫 dom R \| (B \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) \subseteq ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))$
17	3	ad2antrr	$⊢ ((φ \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \land y \in x) \to R : Q ⟶ [0, +∞]$
18		ssrab2	$⊢ \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \subseteq 𝒫 dom R$
19		simplr	$⊢ ((φ \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \land y \in x) \to x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}$
20	18 19	sselid	$⊢ ((φ \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \land y \in x) \to x \in 𝒫 dom R$
21		elpwi	$⊢ x \in 𝒫 dom R \to x \subseteq dom R$
22	20 21	syl	$⊢ ((φ \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \land y \in x) \to x \subseteq dom R$
23	3	fdmd	$⊢ φ \to dom R = Q$
24	23	ad2antrr	$⊢ ((φ \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \land y \in x) \to dom R = Q$
25	22 24	sseqtrd	$⊢ ((φ \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \land y \in x) \to x \subseteq Q$
26		simpr	$⊢ ((φ \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \land y \in x) \to y \in x$
27	25 26	sseldd	$⊢ ((φ \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \land y \in x) \to y \in Q$
28	17 27	ffvelcdmd	$⊢ ((φ \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \land y \in x) \to R (y) \in [0, +∞]$
29	28	ralrimiva	$⊢ (φ \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \to \forall y \in x R (y) \in [0, +∞]$
30		vex	$⊢ x \in V$
31		nfcv	$⊢ \underline{Ⅎ} y x$
32	31	esumcl	$⊢ (x \in V \land \forall y \in x R (y) \in [0, +∞]) \to \underset{y \in x}{\sum^{*}} R (y) \in [0, +∞]$
33	30 32	mpan	$⊢ \forall y \in x R (y) \in [0, +∞] \to \underset{y \in x}{\sum^{*}} R (y) \in [0, +∞]$
34	29 33	syl	$⊢ (φ \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \to \underset{y \in x}{\sum^{*}} R (y) \in [0, +∞]$
35	34	ralrimiva	$⊢ φ \to \forall x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \underset{y \in x}{\sum^{*}} R (y) \in [0, +∞]$
36		eqid	$⊢ (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) = (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))$
37	36	rnmptss	$⊢ \forall x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \underset{y \in x}{\sum^{}} R (y) \in [0, +∞] \to ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) \subseteq [0, +∞]$
38	35 37	syl	$⊢ φ \to ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) \subseteq [0, +∞]$
39	16 38	xrge0infssd	$⊢ φ \to inf (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) [0, +∞] <) \leq inf (ran (x \in \{z \in 𝒫 dom R \| (B \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) [0, +∞] <)$
40	4 5	sstrd	$⊢ φ \to A \subseteq ⋃ Q$
41		omsfval	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land A \subseteq ⋃ Q) \to toOMeas (R) (A) = inf (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) [0, +∞] <)$
42	2 3 40 41	syl3anc	$⊢ φ \to toOMeas (R) (A) = inf (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) [0, +∞] <)$
43		omsfval	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land B \subseteq ⋃ Q) \to toOMeas (R) (B) = inf (ran (x \in \{z \in 𝒫 dom R \| (B \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) [0, +∞] <)$
44	2 3 5 43	syl3anc	$⊢ φ \to toOMeas (R) (B) = inf (ran (x \in \{z \in 𝒫 dom R \| (B \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) [0, +∞] <)$
45	39 42 44	3brtr4d	$⊢ φ \to toOMeas (R) (A) \leq toOMeas (R) (B)$
46	1	fveq1i	$⊢ M (A) = toOMeas (R) (A)$
47	1	fveq1i	$⊢ M (B) = toOMeas (R) (B)$
48	45 46 47	3brtr4g	$⊢ φ \to M (A) \leq M (B)$

Metamath Proof Explorer

Theorem omsmon

Proof