inelcarsg

Description: The Caratheodory measurable sets are closed under intersection. (Contributed by Thierry Arnoux, 18-May-2020)

	Ref	Expression
Hypotheses	carsgval.1	$⊢ φ \to O \in V$
	carsgval.2	$⊢ φ \to M : 𝒫 O ⟶ [0, +∞]$
	difelcarsg.1	$⊢ φ \to A \in toCaraSiga (M)$
	inelcarsg.1	$⊢ (φ \land a \in 𝒫 O \land b \in 𝒫 O) \to M (a \cup b) \leq M (a) +_{𝑒} M (b)$
	inelcarsg.2	$⊢ φ \to B \in toCaraSiga (M)$
Assertion	inelcarsg	$⊢ φ \to A \cap B \in toCaraSiga (M)$

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	$⊢ φ \to O \in V$
2		carsgval.2	$⊢ φ \to M : 𝒫 O ⟶ [0, +∞]$
3		difelcarsg.1	$⊢ φ \to A \in toCaraSiga (M)$
4		inelcarsg.1	$⊢ (φ \land a \in 𝒫 O \land b \in 𝒫 O) \to M (a \cup b) \leq M (a) +_{𝑒} M (b)$
5		inelcarsg.2	$⊢ φ \to B \in toCaraSiga (M)$
6	1 2	elcarsg	$⊢ φ \to (A \in toCaraSiga (M) \leftrightarrow (A \subseteq O \land \forall e \in 𝒫 O M (e \cap A) +_{𝑒} M (e ∖ A) = M (e)))$
7	3 6	mpbid	$⊢ φ \to (A \subseteq O \land \forall e \in 𝒫 O M (e \cap A) +_{𝑒} M (e ∖ A) = M (e))$
8	7	simpld	$⊢ φ \to A \subseteq O$
9		ssinss1	$⊢ A \subseteq O \to A \cap B \subseteq O$
10	8 9	syl	$⊢ φ \to A \cap B \subseteq O$
11		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
12	2	adantr	$⊢ (φ \land e \in 𝒫 O) \to M : 𝒫 O ⟶ [0, +∞]$
13		simpr	$⊢ (φ \land e \in 𝒫 O) \to e \in 𝒫 O$
14	13	elpwdifcl	$⊢ (φ \land e \in 𝒫 O) \to e ∖ (A \cap B) \in 𝒫 O$
15	12 14	ffvelrnd	$⊢ (φ \land e \in 𝒫 O) \to M (e ∖ (A \cap B)) \in [0, +∞]$
16	11 15	sselid	$⊢ (φ \land e \in 𝒫 O) \to M (e ∖ (A \cap B)) \in ℝ^{*}$
17	13	elpwincl1	$⊢ (φ \land e \in 𝒫 O) \to e \cap A \in 𝒫 O$
18	17	elpwdifcl	$⊢ (φ \land e \in 𝒫 O) \to (e \cap A) ∖ B \in 𝒫 O$
19	12 18	ffvelrnd	$⊢ (φ \land e \in 𝒫 O) \to M ((e \cap A) ∖ B) \in [0, +∞]$
20	11 19	sselid	$⊢ (φ \land e \in 𝒫 O) \to M ((e \cap A) ∖ B) \in ℝ^{*}$
21	13	elpwdifcl	$⊢ (φ \land e \in 𝒫 O) \to e ∖ A \in 𝒫 O$
22	12 21	ffvelrnd	$⊢ (φ \land e \in 𝒫 O) \to M (e ∖ A) \in [0, +∞]$
23	11 22	sselid	$⊢ (φ \land e \in 𝒫 O) \to M (e ∖ A) \in ℝ^{*}$
24	20 23	xaddcld	$⊢ (φ \land e \in 𝒫 O) \to M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A) \in ℝ^{*}$
25	13	elpwincl1	$⊢ (φ \land e \in 𝒫 O) \to e \cap (A \cap B) \in 𝒫 O$
26	12 25	ffvelrnd	$⊢ (φ \land e \in 𝒫 O) \to M (e \cap (A \cap B)) \in [0, +∞]$
27	11 26	sselid	$⊢ (φ \land e \in 𝒫 O) \to M (e \cap (A \cap B)) \in ℝ^{*}$
28		indifundif	$⊢ ((e \cap A) ∖ B) \cup (e ∖ A) = e ∖ (A \cap B)$
29	28	fveq2i	$⊢ M (((e \cap A) ∖ B) \cup (e ∖ A)) = M (e ∖ (A \cap B))$
30	4	3expb	$⊢ (φ \land (a \in 𝒫 O \land b \in 𝒫 O)) \to M (a \cup b) \leq M (a) +_{𝑒} M (b)$
31	30	ralrimivva	$⊢ φ \to \forall a \in 𝒫 O \forall b \in 𝒫 O M (a \cup b) \leq M (a) +_{𝑒} M (b)$
32	31	adantr	$⊢ (φ \land e \in 𝒫 O) \to \forall a \in 𝒫 O \forall b \in 𝒫 O M (a \cup b) \leq M (a) +_{𝑒} M (b)$
33		uneq1	$⊢ a = (e \cap A) ∖ B \to a \cup b = ((e \cap A) ∖ B) \cup b$
34	33	fveq2d	$⊢ a = (e \cap A) ∖ B \to M (a \cup b) = M (((e \cap A) ∖ B) \cup b)$
35		fveq2	$⊢ a = (e \cap A) ∖ B \to M (a) = M ((e \cap A) ∖ B)$
36	35	oveq1d	$⊢ a = (e \cap A) ∖ B \to M (a) +_{𝑒} M (b) = M ((e \cap A) ∖ B) +_{𝑒} M (b)$
37	34 36	breq12d	$⊢ a = (e \cap A) ∖ B \to (M (a \cup b) \leq M (a) +_{𝑒} M (b) \leftrightarrow M (((e \cap A) ∖ B) \cup b) \leq M ((e \cap A) ∖ B) +_{𝑒} M (b))$
38		uneq2	$⊢ b = e ∖ A \to ((e \cap A) ∖ B) \cup b = ((e \cap A) ∖ B) \cup (e ∖ A)$
39	38	fveq2d	$⊢ b = e ∖ A \to M (((e \cap A) ∖ B) \cup b) = M (((e \cap A) ∖ B) \cup (e ∖ A))$
40		fveq2	$⊢ b = e ∖ A \to M (b) = M (e ∖ A)$
41	40	oveq2d	$⊢ b = e ∖ A \to M ((e \cap A) ∖ B) +_{𝑒} M (b) = M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A)$
42	39 41	breq12d	$⊢ b = e ∖ A \to (M (((e \cap A) ∖ B) \cup b) \leq M ((e \cap A) ∖ B) +_{𝑒} M (b) \leftrightarrow M (((e \cap A) ∖ B) \cup (e ∖ A)) \leq M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A))$
43	37 42	rspc2v	$⊢ ((e \cap A) ∖ B \in 𝒫 O \land e ∖ A \in 𝒫 O) \to (\forall a \in 𝒫 O \forall b \in 𝒫 O M (a \cup b) \leq M (a) +_{𝑒} M (b) \to M (((e \cap A) ∖ B) \cup (e ∖ A)) \leq M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A))$
44	43	imp	$⊢ (((e \cap A) ∖ B \in 𝒫 O \land e ∖ A \in 𝒫 O) \land \forall a \in 𝒫 O \forall b \in 𝒫 O M (a \cup b) \leq M (a) +_{𝑒} M (b)) \to M (((e \cap A) ∖ B) \cup (e ∖ A)) \leq M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A)$
45	18 21 32 44	syl21anc	$⊢ (φ \land e \in 𝒫 O) \to M (((e \cap A) ∖ B) \cup (e ∖ A)) \leq M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A)$
46	29 45	eqbrtrrid	$⊢ (φ \land e \in 𝒫 O) \to M (e ∖ (A \cap B)) \leq M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A)$
47		xleadd2a	$⊢ ((M (e ∖ (A \cap B)) \in ℝ^{} \land M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A) \in ℝ^{} \land M (e \cap (A \cap B)) \in ℝ^{*}) \land M (e ∖ (A \cap B)) \leq M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A)) \to M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)) \leq M (e \cap (A \cap B)) +_{𝑒} (M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A))$
48	16 24 27 46 47	syl31anc	$⊢ (φ \land e \in 𝒫 O) \to M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)) \leq M (e \cap (A \cap B)) +_{𝑒} (M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A))$
49	1 2	elcarsg	$⊢ φ \to (B \in toCaraSiga (M) \leftrightarrow (B \subseteq O \land \forall f \in 𝒫 O M (f \cap B) +_{𝑒} M (f ∖ B) = M (f)))$
50	5 49	mpbid	$⊢ φ \to (B \subseteq O \land \forall f \in 𝒫 O M (f \cap B) +_{𝑒} M (f ∖ B) = M (f))$
51	50	simprd	$⊢ φ \to \forall f \in 𝒫 O M (f \cap B) +_{𝑒} M (f ∖ B) = M (f)$
52	51	adantr	$⊢ (φ \land e \in 𝒫 O) \to \forall f \in 𝒫 O M (f \cap B) +_{𝑒} M (f ∖ B) = M (f)$
53		ineq1	$⊢ f = e \cap A \to f \cap B = (e \cap A) \cap B$
54	53	fveq2d	$⊢ f = e \cap A \to M (f \cap B) = M ((e \cap A) \cap B)$
55		difeq1	$⊢ f = e \cap A \to f ∖ B = (e \cap A) ∖ B$
56	55	fveq2d	$⊢ f = e \cap A \to M (f ∖ B) = M ((e \cap A) ∖ B)$
57	54 56	oveq12d	$⊢ f = e \cap A \to M (f \cap B) +_{𝑒} M (f ∖ B) = M ((e \cap A) \cap B) +_{𝑒} M ((e \cap A) ∖ B)$
58		fveq2	$⊢ f = e \cap A \to M (f) = M (e \cap A)$
59	57 58	eqeq12d	$⊢ f = e \cap A \to (M (f \cap B) +_{𝑒} M (f ∖ B) = M (f) \leftrightarrow M ((e \cap A) \cap B) +_{𝑒} M ((e \cap A) ∖ B) = M (e \cap A))$
60	59	adantl	$⊢ ((φ \land e \in 𝒫 O) \land f = e \cap A) \to (M (f \cap B) +_{𝑒} M (f ∖ B) = M (f) \leftrightarrow M ((e \cap A) \cap B) +_{𝑒} M ((e \cap A) ∖ B) = M (e \cap A))$
61	17 60	rspcdv	$⊢ (φ \land e \in 𝒫 O) \to (\forall f \in 𝒫 O M (f \cap B) +_{𝑒} M (f ∖ B) = M (f) \to M ((e \cap A) \cap B) +_{𝑒} M ((e \cap A) ∖ B) = M (e \cap A))$
62	52 61	mpd	$⊢ (φ \land e \in 𝒫 O) \to M ((e \cap A) \cap B) +_{𝑒} M ((e \cap A) ∖ B) = M (e \cap A)$
63	62	oveq1d	$⊢ (φ \land e \in 𝒫 O) \to (M ((e \cap A) \cap B) +_{𝑒} M ((e \cap A) ∖ B)) +_{𝑒} M (e ∖ A) = M (e \cap A) +_{𝑒} M (e ∖ A)$
64	17	elpwincl1	$⊢ (φ \land e \in 𝒫 O) \to (e \cap A) \cap B \in 𝒫 O$
65	12 64	ffvelrnd	$⊢ (φ \land e \in 𝒫 O) \to M ((e \cap A) \cap B) \in [0, +∞]$
66		xrge0addass	$⊢ (M ((e \cap A) \cap B) \in [0, +∞] \land M ((e \cap A) ∖ B) \in [0, +∞] \land M (e ∖ A) \in [0, +∞]) \to (M ((e \cap A) \cap B) +_{𝑒} M ((e \cap A) ∖ B)) +_{𝑒} M (e ∖ A) = M ((e \cap A) \cap B) +_{𝑒} (M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A))$
67	65 19 22 66	syl3anc	$⊢ (φ \land e \in 𝒫 O) \to (M ((e \cap A) \cap B) +_{𝑒} M ((e \cap A) ∖ B)) +_{𝑒} M (e ∖ A) = M ((e \cap A) \cap B) +_{𝑒} (M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A))$
68		inass	$⊢ (e \cap A) \cap B = e \cap (A \cap B)$
69	68	fveq2i	$⊢ M ((e \cap A) \cap B) = M (e \cap (A \cap B))$
70	69	oveq1i	$⊢ M ((e \cap A) \cap B) +_{𝑒} (M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A)) = M (e \cap (A \cap B)) +_{𝑒} (M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A))$
71	67 70	eqtrdi	$⊢ (φ \land e \in 𝒫 O) \to (M ((e \cap A) \cap B) +_{𝑒} M ((e \cap A) ∖ B)) +_{𝑒} M (e ∖ A) = M (e \cap (A \cap B)) +_{𝑒} (M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A))$
72	7	simprd	$⊢ φ \to \forall e \in 𝒫 O M (e \cap A) +_{𝑒} M (e ∖ A) = M (e)$
73	72	r19.21bi	$⊢ (φ \land e \in 𝒫 O) \to M (e \cap A) +_{𝑒} M (e ∖ A) = M (e)$
74	63 71 73	3eqtr3d	$⊢ (φ \land e \in 𝒫 O) \to M (e \cap (A \cap B)) +_{𝑒} (M ((e \cap A) ∖ B) +_{𝑒} M (e ∖ A)) = M (e)$
75	48 74	breqtrd	$⊢ (φ \land e \in 𝒫 O) \to M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)) \leq M (e)$
76		inundif	$⊢ (e \cap (A \cap B)) \cup (e ∖ (A \cap B)) = e$
77	76	fveq2i	$⊢ M ((e \cap (A \cap B)) \cup (e ∖ (A \cap B))) = M (e)$
78		uneq1	$⊢ a = e \cap (A \cap B) \to a \cup b = (e \cap (A \cap B)) \cup b$
79	78	fveq2d	$⊢ a = e \cap (A \cap B) \to M (a \cup b) = M ((e \cap (A \cap B)) \cup b)$
80		fveq2	$⊢ a = e \cap (A \cap B) \to M (a) = M (e \cap (A \cap B))$
81	80	oveq1d	$⊢ a = e \cap (A \cap B) \to M (a) +_{𝑒} M (b) = M (e \cap (A \cap B)) +_{𝑒} M (b)$
82	79 81	breq12d	$⊢ a = e \cap (A \cap B) \to (M (a \cup b) \leq M (a) +_{𝑒} M (b) \leftrightarrow M ((e \cap (A \cap B)) \cup b) \leq M (e \cap (A \cap B)) +_{𝑒} M (b))$
83		uneq2	$⊢ b = e ∖ (A \cap B) \to (e \cap (A \cap B)) \cup b = (e \cap (A \cap B)) \cup (e ∖ (A \cap B))$
84	83	fveq2d	$⊢ b = e ∖ (A \cap B) \to M ((e \cap (A \cap B)) \cup b) = M ((e \cap (A \cap B)) \cup (e ∖ (A \cap B)))$
85		fveq2	$⊢ b = e ∖ (A \cap B) \to M (b) = M (e ∖ (A \cap B))$
86	85	oveq2d	$⊢ b = e ∖ (A \cap B) \to M (e \cap (A \cap B)) +_{𝑒} M (b) = M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B))$
87	84 86	breq12d	$⊢ b = e ∖ (A \cap B) \to (M ((e \cap (A \cap B)) \cup b) \leq M (e \cap (A \cap B)) +_{𝑒} M (b) \leftrightarrow M ((e \cap (A \cap B)) \cup (e ∖ (A \cap B))) \leq M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)))$
88	82 87	rspc2v	$⊢ (e \cap (A \cap B) \in 𝒫 O \land e ∖ (A \cap B) \in 𝒫 O) \to (\forall a \in 𝒫 O \forall b \in 𝒫 O M (a \cup b) \leq M (a) +_{𝑒} M (b) \to M ((e \cap (A \cap B)) \cup (e ∖ (A \cap B))) \leq M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)))$
89	88	imp	$⊢ ((e \cap (A \cap B) \in 𝒫 O \land e ∖ (A \cap B) \in 𝒫 O) \land \forall a \in 𝒫 O \forall b \in 𝒫 O M (a \cup b) \leq M (a) +_{𝑒} M (b)) \to M ((e \cap (A \cap B)) \cup (e ∖ (A \cap B))) \leq M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B))$
90	25 14 32 89	syl21anc	$⊢ (φ \land e \in 𝒫 O) \to M ((e \cap (A \cap B)) \cup (e ∖ (A \cap B))) \leq M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B))$
91	77 90	eqbrtrrid	$⊢ (φ \land e \in 𝒫 O) \to M (e) \leq M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B))$
92	75 91	jca	$⊢ (φ \land e \in 𝒫 O) \to (M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)) \leq M (e) \land M (e) \leq M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)))$
93	27 16	xaddcld	$⊢ (φ \land e \in 𝒫 O) \to M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)) \in ℝ^{*}$
94	2	ffvelrnda	$⊢ (φ \land e \in 𝒫 O) \to M (e) \in [0, +∞]$
95	11 94	sselid	$⊢ (φ \land e \in 𝒫 O) \to M (e) \in ℝ^{*}$
96		xrletri3	$⊢ (M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)) \in ℝ^{} \land M (e) \in ℝ^{}) \to (M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)) = M (e) \leftrightarrow (M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)) \leq M (e) \land M (e) \leq M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B))))$
97	93 95 96	syl2anc	$⊢ (φ \land e \in 𝒫 O) \to (M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)) = M (e) \leftrightarrow (M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)) \leq M (e) \land M (e) \leq M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B))))$
98	92 97	mpbird	$⊢ (φ \land e \in 𝒫 O) \to M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)) = M (e)$
99	98	ralrimiva	$⊢ φ \to \forall e \in 𝒫 O M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)) = M (e)$
100	10 99	jca	$⊢ φ \to (A \cap B \subseteq O \land \forall e \in 𝒫 O M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)) = M (e))$
101	1 2	elcarsg	$⊢ φ \to (A \cap B \in toCaraSiga (M) \leftrightarrow (A \cap B \subseteq O \land \forall e \in 𝒫 O M (e \cap (A \cap B)) +_{𝑒} M (e ∖ (A \cap B)) = M (e)))$
102	100 101	mpbird	$⊢ φ \to A \cap B \in toCaraSiga (M)$

Metamath Proof Explorer

Theorem inelcarsg

Proof