Theorem caragenuni

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

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

Proof

Step	Hyp	Ref	Expression
1		caragenuni.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		caragenuni.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3	2	caragenss	⊢ ( 𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂 )
4	1 3	syl	⊢ ( 𝜑 → 𝑆 ⊆ dom 𝑂 )
5	4	unissd	⊢ ( 𝜑 → ∪ 𝑆 ⊆ ∪ dom 𝑂 )
6		eqid	⊢ ∪ dom 𝑂 = ∪ dom 𝑂
7	1 6 2	caragenunidm	⊢ ( 𝜑 → ∪ dom 𝑂 ∈ 𝑆 )
8		elssuni	⊢ ( ∪ dom 𝑂 ∈ 𝑆 → ∪ dom 𝑂 ⊆ ∪ 𝑆 )
9	7 8	syl	⊢ ( 𝜑 → ∪ dom 𝑂 ⊆ ∪ 𝑆 )
10	5 9	eqssd	⊢ ( 𝜑 → ∪ 𝑆 = ∪ dom 𝑂 )