Theorem caragenel2d

Description: Membership in the Caratheodory's construction. Similar to carageneld , but here "less then or equal to" is used, instead of equality. This is Remark 113D of Fremlin1 p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	caragenel2d.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	caragenel2d.x	⊢ 𝑋 = ∪ dom 𝑂
	caragenel2d.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
	caragenel2d.e	⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑋 )
	caragenel2d.a	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) ≤ ( 𝑂 ‘ 𝑎 ) )
Assertion	caragenel2d	⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		caragenel2d.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		caragenel2d.x	⊢ 𝑋 = ∪ dom 𝑂
3		caragenel2d.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
4		caragenel2d.e	⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑋 )
5		caragenel2d.a	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) ≤ ( 𝑂 ‘ 𝑎 ) )
6	1	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝑂 ∈ OutMeas )
7		inss1	⊢ ( 𝑎 ∩ 𝐸 ) ⊆ 𝑎
8		elpwi	⊢ ( 𝑎 ∈ 𝒫 𝑋 → 𝑎 ⊆ 𝑋 )
9	7 8	sstrid	⊢ ( 𝑎 ∈ 𝒫 𝑋 → ( 𝑎 ∩ 𝐸 ) ⊆ 𝑋 )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑎 ∩ 𝐸 ) ⊆ 𝑋 )
11	6 2 10	omexrcl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) ∈ ℝ* )
12	8	ssdifssd	⊢ ( 𝑎 ∈ 𝒫 𝑋 → ( 𝑎 ∖ 𝐸 ) ⊆ 𝑋 )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑎 ∖ 𝐸 ) ⊆ 𝑋 )
14	6 2 13	omexrcl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ∈ ℝ* )
15		xaddcl	⊢ ( ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) ∈ ℝ* ∧ ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ∈ ℝ* ) → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) ∈ ℝ* )
16	11 14 15	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) ∈ ℝ* )
17	8	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝑎 ⊆ 𝑋 )
18	6 2 17	omexrcl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ 𝑎 ) ∈ ℝ* )
19	6 2 17	omelesplit	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ 𝑎 ) ≤ ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) )
20	16 18 5 19	xrletrid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) )
21	1 2 3 4 20	carageneld	⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )