Metamath Proof Explorer

Theorem carsguni

Description: The union of all Caratheodory measurable sets is the universe. (Contributed by Thierry Arnoux, 22-May-2020)

Ref Expression
Hypotheses carsgval.1 ⊢ φ → O ∈ V
carsgval.2 ⊢ φ → M : 𝒫 O ⟶ 0 +∞
baselcarsg.1 ⊢ φ → M ⁡ ∅ = 0
Assertion carsguni ⊢ φ → ⋃ toCaraSiga ⁡ M = O

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ φ → O ∈ V
2 carsgval.2 ⊢ φ → M : 𝒫 O ⟶ 0 +∞
3 baselcarsg.1 ⊢ φ → M ⁡ ∅ = 0
4 1 2 carsgcl ⊢ φ → toCaraSiga ⁡ M ⊆ 𝒫 O
5 4 sselda ⊢ φ ∧ a ∈ toCaraSiga ⁡ M → a ∈ 𝒫 O
6 5 elpwid ⊢ φ ∧ a ∈ toCaraSiga ⁡ M → a ⊆ O
7 6 ralrimiva ⊢ φ → ∀ a ∈ toCaraSiga ⁡ M a ⊆ O
8 unissb ⊢ ⋃ toCaraSiga ⁡ M ⊆ O ↔ ∀ a ∈ toCaraSiga ⁡ M a ⊆ O
9 7 8 sylibr ⊢ φ → ⋃ toCaraSiga ⁡ M ⊆ O
10 1 2 3 baselcarsg ⊢ φ → O ∈ toCaraSiga ⁡ M
11 unissel ⊢ ⋃ toCaraSiga ⁡ M ⊆ O ∧ O ∈ toCaraSiga ⁡ M → ⋃ toCaraSiga ⁡ M = O
12 9 10 11 syl2anc ⊢ φ → ⋃ toCaraSiga ⁡ M = O