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	$⊢ φ \to O \in OutMeas$
	caragenuncl.2	$⊢ S = CaraGen (O)$
	caragenuncl.3	$⊢ φ \to E \in S$
	caragenuncl.4	$⊢ φ \to F \in S$
Assertion	caragenuncl	$⊢ φ \to E \cup F \in S$

Proof

Step	Hyp	Ref	Expression
1		caragenuncl.1	$⊢ φ \to O \in OutMeas$
2		caragenuncl.2	$⊢ S = CaraGen (O)$
3		caragenuncl.3	$⊢ φ \to E \in S$
4		caragenuncl.4	$⊢ φ \to F \in S$
5		eqid	$⊢ ⋃ dom O = ⋃ dom O$
6	1 2 3 5	caragenelss	$⊢ φ \to E \subseteq ⋃ dom O$
7	1 2 4 5	caragenelss	$⊢ φ \to F \subseteq ⋃ dom O$
8	6 7	unssd	$⊢ φ \to E \cup F \subseteq ⋃ dom O$
9	1 5	unidmex	$⊢ φ \to ⋃ dom O \in V$
10		ssexg	$⊢ (E \cup F \subseteq ⋃ dom O \land ⋃ dom O \in V) \to E \cup F \in V$
11	8 9 10	syl2anc	$⊢ φ \to E \cup F \in V$
12		elpwg	$⊢ E \cup F \in V \to (E \cup F \in 𝒫 ⋃ dom O \leftrightarrow E \cup F \subseteq ⋃ dom O)$
13	11 12	syl	$⊢ φ \to (E \cup F \in 𝒫 ⋃ dom O \leftrightarrow E \cup F \subseteq ⋃ dom O)$
14	8 13	mpbird	$⊢ φ \to E \cup F \in 𝒫 ⋃ dom O$
15	1	adantr	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O \in OutMeas$
16	3	adantr	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to E \in S$
17	4	adantr	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to F \in S$
18		elpwi	$⊢ a \in 𝒫 ⋃ dom O \to a \subseteq ⋃ dom O$
19	18	adantl	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to a \subseteq ⋃ dom O$
20	15 2 16 17 5 19	caragenuncllem	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a \cap (E \cup F)) +_{𝑒} O (a ∖ (E \cup F)) = O (a)$
21	1 5 2 14 20	carageneld	$⊢ φ \to E \cup F \in S$

Metamath Proof Explorer

Theorem caragenuncl

Proof