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 φ O OutMeas
caragendifcl.s S = CaraGen O
caragendifcl.e φ E S
Assertion caragendifcl φ S E S

Proof

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