Metamath Proof Explorer


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 φ O OutMeas
caragenuni.s S = CaraGen O
Assertion caragenuni φ S = dom O

Proof

Step Hyp Ref Expression
1 caragenuni.o φ O OutMeas
2 caragenuni.s S = CaraGen O
3 2 caragenss O OutMeas S dom O
4 1 3 syl φ S dom O
5 4 unissd φ S dom O
6 eqid dom O = dom O
7 1 6 2 caragenunidm φ dom O S
8 elssuni dom O S dom O S
9 7 8 syl φ dom O S
10 5 9 eqssd φ S = dom O