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	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	caragenuncl.2	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
	caragenuncl.3	⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
	caragenuncl.4	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
Assertion	caragenuncl	⊢ ( 𝜑 → ( 𝐸 ∪ 𝐹 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		caragenuncl.1	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		caragenuncl.2	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3		caragenuncl.3	⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
4		caragenuncl.4	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
5		eqid	⊢ ∪ dom 𝑂 = ∪ dom 𝑂
6	1 2 3 5	caragenelss	⊢ ( 𝜑 → 𝐸 ⊆ ∪ dom 𝑂 )
7	1 2 4 5	caragenelss	⊢ ( 𝜑 → 𝐹 ⊆ ∪ dom 𝑂 )
8	6 7	unssd	⊢ ( 𝜑 → ( 𝐸 ∪ 𝐹 ) ⊆ ∪ dom 𝑂 )
9	1 5	unidmex	⊢ ( 𝜑 → ∪ dom 𝑂 ∈ V )
10		ssexg	⊢ ( ( ( 𝐸 ∪ 𝐹 ) ⊆ ∪ dom 𝑂 ∧ ∪ dom 𝑂 ∈ V ) → ( 𝐸 ∪ 𝐹 ) ∈ V )
11	8 9 10	syl2anc	⊢ ( 𝜑 → ( 𝐸 ∪ 𝐹 ) ∈ V )
12		elpwg	⊢ ( ( 𝐸 ∪ 𝐹 ) ∈ V → ( ( 𝐸 ∪ 𝐹 ) ∈ 𝒫 ∪ dom 𝑂 ↔ ( 𝐸 ∪ 𝐹 ) ⊆ ∪ dom 𝑂 ) )
13	11 12	syl	⊢ ( 𝜑 → ( ( 𝐸 ∪ 𝐹 ) ∈ 𝒫 ∪ dom 𝑂 ↔ ( 𝐸 ∪ 𝐹 ) ⊆ ∪ dom 𝑂 ) )
14	8 13	mpbird	⊢ ( 𝜑 → ( 𝐸 ∪ 𝐹 ) ∈ 𝒫 ∪ dom 𝑂 )
15	1	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → 𝑂 ∈ OutMeas )
16	3	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → 𝐸 ∈ 𝑆 )
17	4	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → 𝐹 ∈ 𝑆 )
18		elpwi	⊢ ( 𝑎 ∈ 𝒫 ∪ dom 𝑂 → 𝑎 ⊆ ∪ dom 𝑂 )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → 𝑎 ⊆ ∪ dom 𝑂 )
20	15 2 16 17 5 19	caragenuncllem	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ( 𝐸 ∪ 𝐹 ) ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ ( 𝐸 ∪ 𝐹 ) ) ) ) = ( 𝑂 ‘ 𝑎 ) )
21	1 5 2 14 20	carageneld	⊢ ( 𝜑 → ( 𝐸 ∪ 𝐹 ) ∈ 𝑆 )