Theorem caragenunidm

Description: The base set of an outer measure belongs to the sigma-algebra generated by the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	caragenunidm.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	caragenunidm.x	⊢ 𝑋 = ∪ dom 𝑂
	caragenunidm.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
Assertion	caragenunidm	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		caragenunidm.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		caragenunidm.x	⊢ 𝑋 = ∪ dom 𝑂
3		caragenunidm.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
4		dmexg	⊢ ( 𝑂 ∈ OutMeas → dom 𝑂 ∈ V )
5		uniexg	⊢ ( dom 𝑂 ∈ V → ∪ dom 𝑂 ∈ V )
6	1 4 5	3syl	⊢ ( 𝜑 → ∪ dom 𝑂 ∈ V )
7	2 6	eqeltrid	⊢ ( 𝜑 → 𝑋 ∈ V )
8		pwidg	⊢ ( 𝑋 ∈ V → 𝑋 ∈ 𝒫 𝑋 )
9	7 8	syl	⊢ ( 𝜑 → 𝑋 ∈ 𝒫 𝑋 )
10		elpwi	⊢ ( 𝑎 ∈ 𝒫 𝑋 → 𝑎 ⊆ 𝑋 )
11		df-ss	⊢ ( 𝑎 ⊆ 𝑋 ↔ ( 𝑎 ∩ 𝑋 ) = 𝑎 )
12	11	biimpi	⊢ ( 𝑎 ⊆ 𝑋 → ( 𝑎 ∩ 𝑋 ) = 𝑎 )
13	10 12	syl	⊢ ( 𝑎 ∈ 𝒫 𝑋 → ( 𝑎 ∩ 𝑋 ) = 𝑎 )
14	13	fveq2d	⊢ ( 𝑎 ∈ 𝒫 𝑋 → ( 𝑂 ‘ ( 𝑎 ∩ 𝑋 ) ) = ( 𝑂 ‘ 𝑎 ) )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ ( 𝑎 ∩ 𝑋 ) ) = ( 𝑂 ‘ 𝑎 ) )
16		ssdif0	⊢ ( 𝑎 ⊆ 𝑋 ↔ ( 𝑎 ∖ 𝑋 ) = ∅ )
17	10 16	sylib	⊢ ( 𝑎 ∈ 𝒫 𝑋 → ( 𝑎 ∖ 𝑋 ) = ∅ )
18	17	fveq2d	⊢ ( 𝑎 ∈ 𝒫 𝑋 → ( 𝑂 ‘ ( 𝑎 ∖ 𝑋 ) ) = ( 𝑂 ‘ ∅ ) )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ ( 𝑎 ∖ 𝑋 ) ) = ( 𝑂 ‘ ∅ ) )
20	1	ome0	⊢ ( 𝜑 → ( 𝑂 ‘ ∅ ) = 0 )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ ∅ ) = 0 )
22	19 21	eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ ( 𝑎 ∖ 𝑋 ) ) = 0 )
23	15 22	oveq12d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑋 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑋 ) ) ) = ( ( 𝑂 ‘ 𝑎 ) +𝑒 0 ) )
24		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
25	1	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝑂 ∈ OutMeas )
26	10	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝑎 ⊆ 𝑋 )
27	25 2 26	omecl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ 𝑎 ) ∈ ( 0 [,] +∞ ) )
28	24 27	sselid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ 𝑎 ) ∈ ℝ* )
29	28	xaddid1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑂 ‘ 𝑎 ) +𝑒 0 ) = ( 𝑂 ‘ 𝑎 ) )
30		eqidd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑂 ‘ 𝑎 ) = ( 𝑂 ‘ 𝑎 ) )
31	23 29 30	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑋 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑋 ) ) ) = ( 𝑂 ‘ 𝑎 ) )
32	1 2 3 9 31	carageneld	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )