Metamath Proof Explorer

Theorem caragenss

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

Ref Expression
Hypothesis caragenss.1 ⊢ S = CaraGen ⁡ O
Assertion caragenss ⊢ O ∈ OutMeas → S ⊆ dom ⁡ O

Proof

Step Hyp Ref Expression
1 caragenss.1 ⊢ S = CaraGen ⁡ O
2 ssrab2 ⊢ e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a ⊆ 𝒫 ⋃ dom ⁡ O
3 2 a1i ⊢ O ∈ OutMeas → e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a ⊆ 𝒫 ⋃ dom ⁡ O
4 1 a1i ⊢ O ∈ OutMeas → S = CaraGen ⁡ O
5 caragenval ⊢ O ∈ OutMeas → CaraGen ⁡ O = e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a
6 4 5 eqtrd ⊢ O ∈ OutMeas → S = e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a
7 omedm ⊢ O ∈ OutMeas → dom ⁡ O = 𝒫 ⋃ dom ⁡ O
8 6 7 sseq12d ⊢ O ∈ OutMeas → S ⊆ dom ⁡ O ↔ e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a ⊆ 𝒫 ⋃ dom ⁡ O
9 3 8 mpbird ⊢ O ∈ OutMeas → S ⊆ dom ⁡ O