Theorem caragendifcl

Description: The Caratheodory's construction is closed under the complement operation. Second part of Step (b) in the proof of Theorem 113C of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	caragendifcl.o	|- ( ph -> O e. OutMeas )
	caragendifcl.s	|- S = ( CaraGen ` O )
	caragendifcl.e	|- ( ph -> E e. S )
Assertion	caragendifcl	|- ( ph -> ( U. S \ E ) e. S )

Proof

Step	Hyp	Ref	Expression
1		caragendifcl.o	|- ( ph -> O e. OutMeas )
2		caragendifcl.s	|- S = ( CaraGen ` O )
3		caragendifcl.e	|- ( ph -> E e. S )
4		eqid	|- U. dom O = U. dom O
5	2	caragenss	|- ( O e. OutMeas -> S C_ dom O )
6	1 5	syl	|- ( ph -> S C_ dom O )
7	6	unissd	|- ( ph -> U. S C_ U. dom O )
8	7	ssdifssd	|- ( ph -> ( U. S \ E ) C_ U. dom O )
9	2	fvexi	|- S e. _V
10	9	uniex	|- U. S e. _V
11		difexg	|- ( U. S e. _V -> ( U. S \ E ) e. _V )
12	10 11	ax-mp	|- ( U. S \ E ) e. _V
13	12	a1i	|- ( ph -> ( U. S \ E ) e. _V )
14		elpwg	|- ( ( U. S \ E ) e. _V -> ( ( U. S \ E ) e. ~P U. dom O <-> ( U. S \ E ) C_ U. dom O ) )
15	13 14	syl	|- ( ph -> ( ( U. S \ E ) e. ~P U. dom O <-> ( U. S \ E ) C_ U. dom O ) )
16	8 15	mpbird	|- ( ph -> ( U. S \ E ) e. ~P U. dom O )
17		elpwi	|- ( a e. ~P U. dom O -> a C_ U. dom O )
18	17	adantl	|- ( ( ph /\ a e. ~P U. dom O ) -> a C_ U. dom O )
19	1 2	caragenuni	|- ( ph -> U. S = U. dom O )
20	19	eqcomd	|- ( ph -> U. dom O = U. S )
21	20	adantr	|- ( ( ph /\ a e. ~P U. dom O ) -> U. dom O = U. S )
22	18 21	sseqtrd	|- ( ( ph /\ a e. ~P U. dom O ) -> a C_ U. S )
23		difin2	|- ( a C_ U. S -> ( a \ E ) = ( ( U. S \ E ) i^i a ) )
24	22 23	syl	|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ E ) = ( ( U. S \ E ) i^i a ) )
25		incom	|- ( ( U. S \ E ) i^i a ) = ( a i^i ( U. S \ E ) )
26	25	a1i	|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( U. S \ E ) i^i a ) = ( a i^i ( U. S \ E ) ) )
27	24 26	eqtr2d	|- ( ( ph /\ a e. ~P U. dom O ) -> ( a i^i ( U. S \ E ) ) = ( a \ E ) )
28	27	fveq2d	|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a i^i ( U. S \ E ) ) ) = ( O ` ( a \ E ) ) )
29	22	ssdifd	|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ E ) C_ ( U. S \ E ) )
30		sscon	|- ( ( a \ E ) C_ ( U. S \ E ) -> ( a \ ( U. S \ E ) ) C_ ( a \ ( a \ E ) ) )
31	29 30	syl	|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ ( U. S \ E ) ) C_ ( a \ ( a \ E ) ) )
32		dfin4	|- ( a i^i E ) = ( a \ ( a \ E ) )
33	32	a1i	|- ( ( ph /\ a e. ~P U. dom O ) -> ( a i^i E ) = ( a \ ( a \ E ) ) )
34		eqimss2	|- ( ( a i^i E ) = ( a \ ( a \ E ) ) -> ( a \ ( a \ E ) ) C_ ( a i^i E ) )
35	33 34	syl	|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ ( a \ E ) ) C_ ( a i^i E ) )
36	31 35	sstrd	|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ ( U. S \ E ) ) C_ ( a i^i E ) )
37		elinel1	|- ( x e. ( a i^i E ) -> x e. a )
38		elinel2	|- ( x e. ( a i^i E ) -> x e. E )
39		elndif	|- ( x e. E -> -. x e. ( U. S \ E ) )
40	38 39	syl	|- ( x e. ( a i^i E ) -> -. x e. ( U. S \ E ) )
41	37 40	eldifd	|- ( x e. ( a i^i E ) -> x e. ( a \ ( U. S \ E ) ) )
42	41	ssriv	|- ( a i^i E ) C_ ( a \ ( U. S \ E ) )
43	42	a1i	|- ( ( ph /\ a e. ~P U. dom O ) -> ( a i^i E ) C_ ( a \ ( U. S \ E ) ) )
44	36 43	eqssd	|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ ( U. S \ E ) ) = ( a i^i E ) )
45	44	fveq2d	|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a \ ( U. S \ E ) ) ) = ( O ` ( a i^i E ) ) )
46	28 45	oveq12d	|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i ( U. S \ E ) ) ) +e ( O ` ( a \ ( U. S \ E ) ) ) ) = ( ( O ` ( a \ E ) ) +e ( O ` ( a i^i E ) ) ) )
47		iccssxr	|- ( 0 [,] +oo ) C_ RR*
48	1	adantr	|- ( ( ph /\ a e. ~P U. dom O ) -> O e. OutMeas )
49	18	ssdifssd	|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ E ) C_ U. dom O )
50	48 4 49	omecl	|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a \ E ) ) e. ( 0 [,] +oo ) )
51	47 50	sseldi	|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a \ E ) ) e. RR* )
52		ssinss1	|- ( a C_ U. dom O -> ( a i^i E ) C_ U. dom O )
53	17 52	syl	|- ( a e. ~P U. dom O -> ( a i^i E ) C_ U. dom O )
54	53	adantl	|- ( ( ph /\ a e. ~P U. dom O ) -> ( a i^i E ) C_ U. dom O )
55	48 4 54	omecl	|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a i^i E ) ) e. ( 0 [,] +oo ) )
56	47 55	sseldi	|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a i^i E ) ) e. RR* )
57	51 56	xaddcomd	|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a \ E ) ) +e ( O ` ( a i^i E ) ) ) = ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) )
58	1 2	caragenel	|- ( ph -> ( E e. S <-> ( E e. ~P U. dom O /\ A. a e. ~P U. dom O ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) ) ) )
59	3 58	mpbid	|- ( ph -> ( E e. ~P U. dom O /\ A. a e. ~P U. dom O ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) ) )
60	59	simprd	|- ( ph -> A. a e. ~P U. dom O ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) )
61	60	r19.21bi	|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) )
62	46 57 61	3eqtrd	|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i ( U. S \ E ) ) ) +e ( O ` ( a \ ( U. S \ E ) ) ) ) = ( O ` a ) )
63	1 4 2 16 62	carageneld	|- ( ph -> ( U. S \ E ) e. S )