Metamath Proof Explorer

Theorem caragenuncl

Description: The Caratheodory's construction is closed under the union. Step (c) in the proof of Theorem 113C of Fremlin1 p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses caragenuncl.1 ⊢ φ → O ∈ OutMeas
caragenuncl.2 ⊢ S = CaraGen ⁡ O
caragenuncl.3 ⊢ φ → E ∈ S
caragenuncl.4 ⊢ φ → F ∈ S
Assertion caragenuncl ⊢ φ → E ∪ F ∈ S

Proof

Step Hyp Ref Expression
1 caragenuncl.1 ⊢ φ → O ∈ OutMeas
2 caragenuncl.2 ⊢ S = CaraGen ⁡ O
3 caragenuncl.3 ⊢ φ → E ∈ S
4 caragenuncl.4 ⊢ φ → F ∈ S
5 eqid ⊢ ⋃ dom ⁡ O = ⋃ dom ⁡ O
6 1 2 3 5 caragenelss ⊢ φ → E ⊆ ⋃ dom ⁡ O
7 1 2 4 5 caragenelss ⊢ φ → F ⊆ ⋃ dom ⁡ O
8 6 7 unssd ⊢ φ → E ∪ F ⊆ ⋃ dom ⁡ O
9 1 5 unidmex ⊢ φ → ⋃ dom ⁡ O ∈ V
10 ssexg ⊢ E ∪ F ⊆ ⋃ dom ⁡ O ∧ ⋃ dom ⁡ O ∈ V → E ∪ F ∈ V
11 8 9 10 syl2anc ⊢ φ → E ∪ F ∈ V
12 elpwg ⊢ E ∪ F ∈ V → E ∪ F ∈ 𝒫 ⋃ dom ⁡ O ↔ E ∪ F ⊆ ⋃ dom ⁡ O
13 11 12 syl ⊢ φ → E ∪ F ∈ 𝒫 ⋃ dom ⁡ O ↔ E ∪ F ⊆ ⋃ dom ⁡ O
14 8 13 mpbird ⊢ φ → E ∪ F ∈ 𝒫 ⋃ dom ⁡ O
15 1 adantr ⊢ φ ∧ a ∈ 𝒫 ⋃ dom ⁡ O → O ∈ OutMeas
16 3 adantr ⊢ φ ∧ a ∈ 𝒫 ⋃ dom ⁡ O → E ∈ S
17 4 adantr ⊢ φ ∧ a ∈ 𝒫 ⋃ dom ⁡ O → F ∈ S
18 elpwi ⊢ a ∈ 𝒫 ⋃ dom ⁡ O → a ⊆ ⋃ dom ⁡ O
19 18 adantl ⊢ φ ∧ a ∈ 𝒫 ⋃ dom ⁡ O → a ⊆ ⋃ dom ⁡ O
20 15 2 16 17 5 19 caragenuncllem ⊢ φ ∧ a ∈ 𝒫 ⋃ dom ⁡ O → O ⁡ a ∩ E ∪ F + 𝑒 O ⁡ a ∖ E ∪ F = O ⁡ a
21 1 5 2 14 20 carageneld ⊢ φ → E ∪ F ∈ S