Theorem 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	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	omeunle.x	⊢ 𝑋 = ∪ dom 𝑂
	omeunle.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
	omeunle.b	⊢ ( 𝜑 → 𝐵 ⊆ 𝑋 )
Assertion	omeunle	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( 𝑂 ‘ 𝐴 ) +𝑒 ( 𝑂 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		omeunle.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		omeunle.x	⊢ 𝑋 = ∪ dom 𝑂
3		omeunle.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
4		omeunle.b	⊢ ( 𝜑 → 𝐵 ⊆ 𝑋 )
5	1 2	unidmex	⊢ ( 𝜑 → 𝑋 ∈ V )
6		ssexg	⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ V ) → 𝐴 ∈ V )
7	3 5 6	syl2anc	⊢ ( 𝜑 → 𝐴 ∈ V )
8		ssexg	⊢ ( ( 𝐵 ⊆ 𝑋 ∧ 𝑋 ∈ V ) → 𝐵 ∈ V )
9	4 5 8	syl2anc	⊢ ( 𝜑 → 𝐵 ∈ V )
10		uniprg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
11	7 9 10	syl2anc	⊢ ( 𝜑 → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
12	11	eqcomd	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) = ∪ { 𝐴 , 𝐵 } )
13	12	fveq2d	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( 𝑂 ‘ ∪ { 𝐴 , 𝐵 } ) )
14		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
15	3 4	unssd	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ⊆ 𝑋 )
16	11 15	eqsstrd	⊢ ( 𝜑 → ∪ { 𝐴 , 𝐵 } ⊆ 𝑋 )
17	1 2 16	omecl	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ { 𝐴 , 𝐵 } ) ∈ ( 0 [,] +∞ ) )
18	14 17	sselid	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ { 𝐴 , 𝐵 } ) ∈ ℝ* )
19		prfi	⊢ { 𝐴 , 𝐵 } ∈ Fin
20	19	elexi	⊢ { 𝐴 , 𝐵 } ∈ V
21	20	a1i	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ V )
22	1 2	omef	⊢ ( 𝜑 → 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
23		elpwg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
24	7 23	syl	⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
25	3 24	mpbird	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝑋 )
26		elpwg	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ 𝒫 𝑋 ↔ 𝐵 ⊆ 𝑋 ) )
27	9 26	syl	⊢ ( 𝜑 → ( 𝐵 ∈ 𝒫 𝑋 ↔ 𝐵 ⊆ 𝑋 ) )
28	4 27	mpbird	⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝑋 )
29	25 28	jca	⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 𝑋 ∧ 𝐵 ∈ 𝒫 𝑋 ) )
30		prssg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 𝐴 ∈ 𝒫 𝑋 ∧ 𝐵 ∈ 𝒫 𝑋 ) ↔ { 𝐴 , 𝐵 } ⊆ 𝒫 𝑋 ) )
31	7 9 30	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ∈ 𝒫 𝑋 ∧ 𝐵 ∈ 𝒫 𝑋 ) ↔ { 𝐴 , 𝐵 } ⊆ 𝒫 𝑋 ) )
32	29 31	mpbid	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ 𝒫 𝑋 )
33	22 32	fssresd	⊢ ( 𝜑 → ( 𝑂 ↾ { 𝐴 , 𝐵 } ) : { 𝐴 , 𝐵 } ⟶ ( 0 [,] +∞ ) )
34	21 33	sge0xrcl	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑂 ↾ { 𝐴 , 𝐵 } ) ) ∈ ℝ* )
35	1 2 3	omecl	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
36	14 35	sselid	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℝ* )
37	1 2 4	omecl	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
38	14 37	sselid	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) ∈ ℝ* )
39	36 38	xaddcld	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐴 ) +𝑒 ( 𝑂 ‘ 𝐵 ) ) ∈ ℝ* )
40		isfinite	⊢ ( { 𝐴 , 𝐵 } ∈ Fin ↔ { 𝐴 , 𝐵 } ≺ ω )
41	40	biimpi	⊢ ( { 𝐴 , 𝐵 } ∈ Fin → { 𝐴 , 𝐵 } ≺ ω )
42		sdomdom	⊢ ( { 𝐴 , 𝐵 } ≺ ω → { 𝐴 , 𝐵 } ≼ ω )
43	41 42	syl	⊢ ( { 𝐴 , 𝐵 } ∈ Fin → { 𝐴 , 𝐵 } ≼ ω )
44	19 43	ax-mp	⊢ { 𝐴 , 𝐵 } ≼ ω
45	44	a1i	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ≼ ω )
46	1 2 32 45	omeunile	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ { 𝐴 , 𝐵 } ) ≤ ( Σ^ ‘ ( 𝑂 ↾ { 𝐴 , 𝐵 } ) ) )
47	22 32	feqresmpt	⊢ ( 𝜑 → ( 𝑂 ↾ { 𝐴 , 𝐵 } ) = ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ ( 𝑂 ‘ 𝑘 ) ) )
48	47	fveq2d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑂 ↾ { 𝐴 , 𝐵 } ) ) = ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ ( 𝑂 ‘ 𝑘 ) ) ) )
49		fveq2	⊢ ( 𝑘 = 𝐴 → ( 𝑂 ‘ 𝑘 ) = ( 𝑂 ‘ 𝐴 ) )
50		fveq2	⊢ ( 𝑘 = 𝐵 → ( 𝑂 ‘ 𝑘 ) = ( 𝑂 ‘ 𝐵 ) )
51	7 9 35 37 49 50	sge0prle	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↦ ( 𝑂 ‘ 𝑘 ) ) ) ≤ ( ( 𝑂 ‘ 𝐴 ) +𝑒 ( 𝑂 ‘ 𝐵 ) ) )
52	48 51	eqbrtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑂 ↾ { 𝐴 , 𝐵 } ) ) ≤ ( ( 𝑂 ‘ 𝐴 ) +𝑒 ( 𝑂 ‘ 𝐵 ) ) )
53	18 34 39 46 52	xrletrd	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ { 𝐴 , 𝐵 } ) ≤ ( ( 𝑂 ‘ 𝐴 ) +𝑒 ( 𝑂 ‘ 𝐵 ) ) )
54	13 53	eqbrtrd	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( 𝑂 ‘ 𝐴 ) +𝑒 ( 𝑂 ‘ 𝐵 ) ) )