Theorem caragensspw

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

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

Proof

Step	Hyp	Ref	Expression
1		caragensspw.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		caragensspw.x	⊢ 𝑋 = ∪ dom 𝑂
3		caragensspw.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
4	3	caragenss	⊢ ( 𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂 )
5	1 4	syl	⊢ ( 𝜑 → 𝑆 ⊆ dom 𝑂 )
6		pwuni	⊢ dom 𝑂 ⊆ 𝒫 ∪ dom 𝑂
7	6	a1i	⊢ ( 𝜑 → dom 𝑂 ⊆ 𝒫 ∪ dom 𝑂 )
8	5 7	sstrd	⊢ ( 𝜑 → 𝑆 ⊆ 𝒫 ∪ dom 𝑂 )
9	2	pweqi	⊢ 𝒫 𝑋 = 𝒫 ∪ dom 𝑂
10	9	eqcomi	⊢ 𝒫 ∪ dom 𝑂 = 𝒫 𝑋
11	10	a1i	⊢ ( 𝜑 → 𝒫 ∪ dom 𝑂 = 𝒫 𝑋 )
12	8 11	sseqtrd	⊢ ( 𝜑 → 𝑆 ⊆ 𝒫 𝑋 )