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	|- ( ph -> O e. OutMeas )
	caragenuncl.2	|- S = ( CaraGen ` O )
	caragenuncl.3	|- ( ph -> E e. S )
	caragenuncl.4	|- ( ph -> F e. S )
Assertion	caragenuncl	|- ( ph -> ( E u. F ) e. S )

Proof

Step	Hyp	Ref	Expression
1		caragenuncl.1	|- ( ph -> O e. OutMeas )
2		caragenuncl.2	|- S = ( CaraGen ` O )
3		caragenuncl.3	|- ( ph -> E e. S )
4		caragenuncl.4	|- ( ph -> F e. S )
5		eqid	|- U. dom O = U. dom O
6	1 2 3 5	caragenelss	|- ( ph -> E C_ U. dom O )
7	1 2 4 5	caragenelss	|- ( ph -> F C_ U. dom O )
8	6 7	unssd	|- ( ph -> ( E u. F ) C_ U. dom O )
9	1 5	unidmex	|- ( ph -> U. dom O e. _V )
10		ssexg	|- ( ( ( E u. F ) C_ U. dom O /\ U. dom O e. _V ) -> ( E u. F ) e. _V )
11	8 9 10	syl2anc	|- ( ph -> ( E u. F ) e. _V )
12		elpwg	|- ( ( E u. F ) e. _V -> ( ( E u. F ) e. ~P U. dom O <-> ( E u. F ) C_ U. dom O ) )
13	11 12	syl	|- ( ph -> ( ( E u. F ) e. ~P U. dom O <-> ( E u. F ) C_ U. dom O ) )
14	8 13	mpbird	|- ( ph -> ( E u. F ) e. ~P U. dom O )
15	1	adantr	|- ( ( ph /\ a e. ~P U. dom O ) -> O e. OutMeas )
16	3	adantr	|- ( ( ph /\ a e. ~P U. dom O ) -> E e. S )
17	4	adantr	|- ( ( ph /\ a e. ~P U. dom O ) -> F e. S )
18		elpwi	|- ( a e. ~P U. dom O -> a C_ U. dom O )
19	18	adantl	|- ( ( ph /\ a e. ~P U. dom O ) -> a C_ U. dom O )
20	15 2 16 17 5 19	caragenuncllem	|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i ( E u. F ) ) ) +e ( O ` ( a \ ( E u. F ) ) ) ) = ( O ` a ) )
21	1 5 2 14 20	carageneld	|- ( ph -> ( E u. F ) e. S )