omssubaddlem

Description: For any small margin E , we can find a covering approaching the outer measure of a set A by that margin. (Contributed by Thierry Arnoux, 18-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, +∞]$
	omssubaddlem.a	$⊢ φ \to A \subseteq ⋃ Q$
	omssubaddlem.m	$⊢ φ \to M (A) \in ℝ$
	omssubaddlem.e	$⊢ φ \to E \in ℝ^{+}$
Assertion	omssubaddlem	$⊢ φ \to \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \underset{w \in x}{\sum^{*}} R (w) < M (A) + E$

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		omssubaddlem.a	$⊢ φ \to A \subseteq ⋃ Q$
5		omssubaddlem.m	$⊢ φ \to M (A) \in ℝ$
6		omssubaddlem.e	$⊢ φ \to E \in ℝ^{+}$
7	6	rpred	$⊢ φ \to E \in ℝ$
8	5 7	readdcld	$⊢ φ \to M (A) + E \in ℝ$
9	8	rexrd	$⊢ φ \to M (A) + E \in ℝ^{*}$
10		omsf	$⊢ (Q \in V \land R : Q ⟶ [0, +∞]) \to toOMeas (R) : 𝒫 ⋃ dom R ⟶ [0, +∞]$
11	2 3 10	syl2anc	$⊢ φ \to toOMeas (R) : 𝒫 ⋃ dom R ⟶ [0, +∞]$
12	1	feq1i	$⊢ M : 𝒫 ⋃ dom R ⟶ [0, +∞] \leftrightarrow toOMeas (R) : 𝒫 ⋃ dom R ⟶ [0, +∞]$
13	11 12	sylibr	$⊢ φ \to M : 𝒫 ⋃ dom R ⟶ [0, +∞]$
14	3	fdmd	$⊢ φ \to dom R = Q$
15	14	unieqd	$⊢ φ \to ⋃ dom R = ⋃ Q$
16	4 15	sseqtrrd	$⊢ φ \to A \subseteq ⋃ dom R$
17	2	uniexd	$⊢ φ \to ⋃ Q \in V$
18	4 17	jca	$⊢ φ \to (A \subseteq ⋃ Q \land ⋃ Q \in V)$
19		ssexg	$⊢ (A \subseteq ⋃ Q \land ⋃ Q \in V) \to A \in V$
20		elpwg	$⊢ A \in V \to (A \in 𝒫 ⋃ dom R \leftrightarrow A \subseteq ⋃ dom R)$
21	18 19 20	3syl	$⊢ φ \to (A \in 𝒫 ⋃ dom R \leftrightarrow A \subseteq ⋃ dom R)$
22	16 21	mpbird	$⊢ φ \to A \in 𝒫 ⋃ dom R$
23	13 22	ffvelrnd	$⊢ φ \to M (A) \in [0, +∞]$
24		elxrge0	$⊢ M (A) \in [0, +∞] \leftrightarrow (M (A) \in ℝ^{*} \land 0 \leq M (A))$
25	24	simprbi	$⊢ M (A) \in [0, +∞] \to 0 \leq M (A)$
26	23 25	syl	$⊢ φ \to 0 \leq M (A)$
27	6	rpge0d	$⊢ φ \to 0 \leq E$
28	5 7 26 27	addge0d	$⊢ φ \to 0 \leq M (A) + E$
29		elxrge0	$⊢ M (A) + E \in [0, +∞] \leftrightarrow (M (A) + E \in ℝ^{*} \land 0 \leq M (A) + E)$
30	9 28 29	sylanbrc	$⊢ φ \to M (A) + E \in [0, +∞]$
31	1	fveq1i	$⊢ M (A) = toOMeas (R) (A)$
32		omsfval	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land A \subseteq ⋃ Q) \to toOMeas (R) (A) = sup (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <)$
33	2 3 4 32	syl3anc	$⊢ φ \to toOMeas (R) (A) = sup (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <)$
34	31 33	eqtr2id	$⊢ φ \to sup (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <) = M (A)$
35	5 6	ltaddrpd	$⊢ φ \to M (A) < M (A) + E$
36	34 35	eqbrtrd	$⊢ φ \to sup (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <) < M (A) + E$
37		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
38		xrltso	$⊢ < Or ℝ^{*}$
39		soss	$⊢ [0, +∞] \subseteq ℝ^{} \to (< Or ℝ^{} \to < Or [0, +∞])$
40	37 38 39	mp2	$⊢ < Or [0, +∞]$
41	40	a1i	$⊢ φ \to < Or [0, +∞]$
42		omscl	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \to ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) \subseteq [0, +∞]$
43	2 3 22 42	syl3anc	$⊢ φ \to ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) \subseteq [0, +∞]$
44		xrge0infss	$⊢ ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \subseteq [0, +∞] \to \exists e \in [0, +∞] (\forall t \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \neg t < e \land \forall t \in [0, +∞] (e < t \to \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) u < t))$
45	43 44	syl	$⊢ φ \to \exists e \in [0, +∞] (\forall t \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \neg t < e \land \forall t \in [0, +∞] (e < t \to \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) u < t))$
46	41 45	infglb	$⊢ φ \to ((M (A) + E \in [0, +∞] \land sup (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) [0, +∞] <) < M (A) + E) \to \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) u < M (A) + E)$
47	30 36 46	mp2and	$⊢ φ \to \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) u < M (A) + E$
48		eqid	$⊢ (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) = (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w))$
49		esumex	$⊢ \underset{w \in x}{\sum^{*}} R (w) \in V$
50	48 49	elrnmpti	$⊢ u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \leftrightarrow \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} u = \underset{w \in x}{\sum^{}} R (w)$
51	50	anbi1i	$⊢ (u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \land u < M (A) + E) \leftrightarrow (\exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + E)$
52		r19.41v	$⊢ \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + E) \leftrightarrow (\exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + E)$
53	51 52	bitr4i	$⊢ (u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \land u < M (A) + E) \leftrightarrow \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + E)$
54	53	exbii	$⊢ \exists u (u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \land u < M (A) + E) \leftrightarrow \exists u \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + E)$
55		df-rex	$⊢ \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) u < M (A) + E \leftrightarrow \exists u (u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \land u < M (A) + E)$
56		rexcom4	$⊢ \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \exists u (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + E) \leftrightarrow \exists u \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + E)$
57	54 55 56	3bitr4i	$⊢ \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) u < M (A) + E \leftrightarrow \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \exists u (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + E)$
58		breq1	$⊢ u = \underset{w \in x}{\sum^{}} R (w) \to (u < M (A) + E \leftrightarrow \underset{w \in x}{\sum^{}} R (w) < M (A) + E)$
59	58	biimpa	$⊢ (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + E) \to \underset{w \in x}{\sum^{}} R (w) < M (A) + E$
60	59	exlimiv	$⊢ \exists u (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + E) \to \underset{w \in x}{\sum^{}} R (w) < M (A) + E$
61	60	reximi	$⊢ \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \exists u (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + E) \to \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \underset{w \in x}{\sum^{}} R (w) < M (A) + E$
62	57 61	sylbi	$⊢ \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) u < M (A) + E \to \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \underset{w \in x}{\sum^{}} R (w) < M (A) + E$
63	47 62	syl	$⊢ φ \to \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \underset{w \in x}{\sum^{*}} R (w) < M (A) + E$

Metamath Proof Explorer

Theorem omssubaddlem

Proof