omeunle

Description: The outer measure of the union of two sets is less than or equal to the sum of the measures, Remark 113B (c) of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	omeunle.o	$⊢ φ \to O \in OutMeas$
	omeunle.x	$⊢ X = ⋃ dom O$
	omeunle.a	$⊢ φ \to A \subseteq X$
	omeunle.b	$⊢ φ \to B \subseteq X$
Assertion	omeunle	$⊢ φ \to O (A \cup B) \leq O (A) +_{𝑒} O (B)$

Proof

Step	Hyp	Ref	Expression
1		omeunle.o	$⊢ φ \to O \in OutMeas$
2		omeunle.x	$⊢ X = ⋃ dom O$
3		omeunle.a	$⊢ φ \to A \subseteq X$
4		omeunle.b	$⊢ φ \to B \subseteq X$
5	1 2	unidmex	$⊢ φ \to X \in V$
6		ssexg	$⊢ (A \subseteq X \land X \in V) \to A \in V$
7	3 5 6	syl2anc	$⊢ φ \to A \in V$
8		ssexg	$⊢ (B \subseteq X \land X \in V) \to B \in V$
9	4 5 8	syl2anc	$⊢ φ \to B \in V$
10		uniprg	$⊢ (A \in V \land B \in V) \to ⋃ \{A, B\} = A \cup B$
11	7 9 10	syl2anc	$⊢ φ \to ⋃ \{A, B\} = A \cup B$
12	11	eqcomd	$⊢ φ \to A \cup B = ⋃ \{A, B\}$
13	12	fveq2d	$⊢ φ \to O (A \cup B) = O (⋃ \{A, B\})$
14		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
15	3 4	unssd	$⊢ φ \to A \cup B \subseteq X$
16	11 15	eqsstrd	$⊢ φ \to ⋃ \{A, B\} \subseteq X$
17	1 2 16	omecl	$⊢ φ \to O (⋃ \{A, B\}) \in [0, +∞]$
18	14 17	sselid	$⊢ φ \to O (⋃ \{A, B\}) \in ℝ^{*}$
19		prfi	$⊢ \{A, B\} \in Fin$
20	19	elexi	$⊢ \{A, B\} \in V$
21	20	a1i	$⊢ φ \to \{A, B\} \in V$
22	1 2	omef	$⊢ φ \to O : 𝒫 X ⟶ [0, +∞]$
23		elpwg	$⊢ A \in V \to (A \in 𝒫 X \leftrightarrow A \subseteq X)$
24	7 23	syl	$⊢ φ \to (A \in 𝒫 X \leftrightarrow A \subseteq X)$
25	3 24	mpbird	$⊢ φ \to A \in 𝒫 X$
26		elpwg	$⊢ B \in V \to (B \in 𝒫 X \leftrightarrow B \subseteq X)$
27	9 26	syl	$⊢ φ \to (B \in 𝒫 X \leftrightarrow B \subseteq X)$
28	4 27	mpbird	$⊢ φ \to B \in 𝒫 X$
29	25 28	jca	$⊢ φ \to (A \in 𝒫 X \land B \in 𝒫 X)$
30		prssg	$⊢ (A \in V \land B \in V) \to ((A \in 𝒫 X \land B \in 𝒫 X) \leftrightarrow \{A, B\} \subseteq 𝒫 X)$
31	7 9 30	syl2anc	$⊢ φ \to ((A \in 𝒫 X \land B \in 𝒫 X) \leftrightarrow \{A, B\} \subseteq 𝒫 X)$
32	29 31	mpbid	$⊢ φ \to \{A, B\} \subseteq 𝒫 X$
33	22 32	fssresd	$⊢ φ \to ({O ↾}_{\{A, B\}}) : \{A, B\} ⟶ [0, +∞]$
34	21 33	sge0xrcl	$⊢ φ \to sum^({O ↾}_{\{A, B\}}) \in ℝ^{*}$
35	1 2 3	omecl	$⊢ φ \to O (A) \in [0, +∞]$
36	14 35	sselid	$⊢ φ \to O (A) \in ℝ^{*}$
37	1 2 4	omecl	$⊢ φ \to O (B) \in [0, +∞]$
38	14 37	sselid	$⊢ φ \to O (B) \in ℝ^{*}$
39	36 38	xaddcld	$⊢ φ \to O (A) +_{𝑒} O (B) \in ℝ^{*}$
40		isfinite	$⊢ \{A, B\} \in Fin \leftrightarrow \{A, B\} ≺ ω$
41	40	biimpi	$⊢ \{A, B\} \in Fin \to \{A, B\} ≺ ω$
42		sdomdom	$⊢ \{A, B\} ≺ ω \to \{A, B\} ≼ ω$
43	41 42	syl	$⊢ \{A, B\} \in Fin \to \{A, B\} ≼ ω$
44	19 43	ax-mp	$⊢ \{A, B\} ≼ ω$
45	44	a1i	$⊢ φ \to \{A, B\} ≼ ω$
46	1 2 32 45	omeunile	$⊢ φ \to O (⋃ \{A, B\}) \leq sum^({O ↾}_{\{A, B\}})$
47	22 32	feqresmpt	$⊢ φ \to {O ↾}_{\{A, B\}} = (k \in \{A, B\} ⟼ O (k))$
48	47	fveq2d	$⊢ φ \to sum^({O ↾}_{\{A, B\}}) = sum^((k \in \{A, B\} ⟼ O (k)))$
49		fveq2	$⊢ k = A \to O (k) = O (A)$
50		fveq2	$⊢ k = B \to O (k) = O (B)$
51	7 9 35 37 49 50	sge0prle	$⊢ φ \to sum^((k \in \{A, B\} ⟼ O (k))) \leq O (A) +_{𝑒} O (B)$
52	48 51	eqbrtrd	$⊢ φ \to sum^({O ↾}_{\{A, B\}}) \leq O (A) +_{𝑒} O (B)$
53	18 34 39 46 52	xrletrd	$⊢ φ \to O (⋃ \{A, B\}) \leq O (A) +_{𝑒} O (B)$
54	13 53	eqbrtrd	$⊢ φ \to O (A \cup B) \leq O (A) +_{𝑒} O (B)$

Metamath Proof Explorer

Theorem omeunle

Proof