Metamath Proof Explorer


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 sselid
 |-  ( ( 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 sselid
 |-  ( ( 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 )