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	$⊢ φ \to O \in OutMeas$
	caragendifcl.s	$⊢ S = CaraGen (O)$
	caragendifcl.e	$⊢ φ \to E \in S$
Assertion	caragendifcl	$⊢ φ \to ⋃ S ∖ E \in S$

Proof

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

Metamath Proof Explorer

Theorem caragendifcl

Proof