caragencmpl

Description: A measure built with the Caratheodory's construction is complete. See Definition 112Df of Fremlin1 p. 19. This is Exercise 113Xa of Fremlin1 p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	caragencmpl.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	caragencmpl.x	⊢ 𝑋 = ∪ dom 𝑂
	caragencmpl.e	⊢ ( 𝜑 → 𝐸 ⊆ 𝑋 )
	caragencmpl.z	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐸 ) = 0 )
	caragencmpl.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
Assertion	caragencmpl	⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		caragencmpl.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		caragencmpl.x	⊢ 𝑋 = ∪ dom 𝑂
3		caragencmpl.e	⊢ ( 𝜑 → 𝐸 ⊆ 𝑋 )
4		caragencmpl.z	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐸 ) = 0 )
5		caragencmpl.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
6	1 2	unidmex	⊢ ( 𝜑 → 𝑋 ∈ V )
7	6 3	ssexd	⊢ ( 𝜑 → 𝐸 ∈ V )
8		elpwg	⊢ ( 𝐸 ∈ V → ( 𝐸 ∈ 𝒫 𝑋 ↔ 𝐸 ⊆ 𝑋 ) )
9	7 8	syl	⊢ ( 𝜑 → ( 𝐸 ∈ 𝒫 𝑋 ↔ 𝐸 ⊆ 𝑋 ) )
10	3 9	mpbird	⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑋 )
11	1	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝑂 ∈ OutMeas )
12	3	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝐸 ⊆ 𝑋 )
13	4	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ 𝐸 ) = 0 )
14		inss2	⊢ ( 𝑎 ∩ 𝐸 ) ⊆ 𝐸
15	14	a1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑎 ∩ 𝐸 ) ⊆ 𝐸 )
16	11 2 12 13 15	omess0	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) = 0 )
17	16	oveq1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +_𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 0 +_𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) )
18		difssd	⊢ ( 𝑎 ∈ 𝒫 𝑋 → ( 𝑎 ∖ 𝐸 ) ⊆ 𝑎 )
19		elpwi	⊢ ( 𝑎 ∈ 𝒫 𝑋 → 𝑎 ⊆ 𝑋 )
20	18 19	sstrd	⊢ ( 𝑎 ∈ 𝒫 𝑋 → ( 𝑎 ∖ 𝐸 ) ⊆ 𝑋 )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑎 ∖ 𝐸 ) ⊆ 𝑋 )
22	11 2 21	omexrcl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ∈ ℝ^* )
23		xaddid2	⊢ ( ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ∈ ℝ^* → ( 0 +_𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) )
24	22 23	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 0 +_𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) )
25	17 24	eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +_𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) )
26	19	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝑎 ⊆ 𝑋 )
27	18	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑎 ∖ 𝐸 ) ⊆ 𝑎 )
28	11 2 26 27	omessle	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ≤ ( 𝑂 ‘ 𝑎 ) )
29	25 28	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +_𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) ≤ ( 𝑂 ‘ 𝑎 ) )
30	1 2 5 10 29	caragenel2d	⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )

Metamath Proof Explorer

Theorem caragencmpl

Proof