Theorem inelcarsg

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

	Ref	Expression
Hypotheses	carsgval.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
	carsgval.2	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
	difelcarsg.1	⊢ ( 𝜑 → 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )
	inelcarsg.1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑂 ∧ 𝑏 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +e ( 𝑀 ‘ 𝑏 ) ) )
	inelcarsg.2	⊢ ( 𝜑 → 𝐵 ∈ ( toCaraSiga ‘ 𝑀 ) )
Assertion	inelcarsg	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ ( toCaraSiga ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2		carsgval.2	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3		difelcarsg.1	⊢ ( 𝜑 → 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )
4		inelcarsg.1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑂 ∧ 𝑏 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +e ( 𝑀 ‘ 𝑏 ) ) )
5		inelcarsg.2	⊢ ( 𝜑 → 𝐵 ∈ ( toCaraSiga ‘ 𝑀 ) )
6	1 2	elcarsg	⊢ ( 𝜑 → ( 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( 𝐴 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )
7	3 6	mpbid	⊢ ( 𝜑 → ( 𝐴 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) )
8	7	simpld	⊢ ( 𝜑 → 𝐴 ⊆ 𝑂 )
9		ssinss1	⊢ ( 𝐴 ⊆ 𝑂 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝑂 )
10	8 9	syl	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝑂 )
11		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
12	2	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → 𝑒 ∈ 𝒫 𝑂 )
14	13	elpwdifcl	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ∈ 𝒫 𝑂 )
15	12 14	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∈ ( 0 [,] +∞ ) )
16	11 15	sselid	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∈ ℝ* )
17	13	elpwincl1	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∩ 𝐴 ) ∈ 𝒫 𝑂 )
18	17	elpwdifcl	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∈ 𝒫 𝑂 )
19	12 18	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
20	11 19	sselid	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) ∈ ℝ* )
21	13	elpwdifcl	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∖ 𝐴 ) ∈ 𝒫 𝑂 )
22	12 21	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
23	11 22	sselid	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ∈ ℝ* )
24	20 23	xaddcld	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) ∈ ℝ* )
25	13	elpwincl1	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∈ 𝒫 𝑂 )
26	12 25	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) ∈ ( 0 [,] +∞ ) )
27	11 26	sselid	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) ∈ ℝ* )
28		indifundif	⊢ ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∪ ( 𝑒 ∖ 𝐴 ) ) = ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) )
29	28	fveq2i	⊢ ( 𝑀 ‘ ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∪ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) )
30	4	3expb	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝒫 𝑂 ∧ 𝑏 ∈ 𝒫 𝑂 ) ) → ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +e ( 𝑀 ‘ 𝑏 ) ) )
31	30	ralrimivva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 𝑂 ∀ 𝑏 ∈ 𝒫 𝑂 ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +e ( 𝑀 ‘ 𝑏 ) ) )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ∀ 𝑎 ∈ 𝒫 𝑂 ∀ 𝑏 ∈ 𝒫 𝑂 ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +e ( 𝑀 ‘ 𝑏 ) ) )
33		uneq1	⊢ ( 𝑎 = ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) → ( 𝑎 ∪ 𝑏 ) = ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∪ 𝑏 ) )
34	33	fveq2d	⊢ ( 𝑎 = ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) → ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) = ( 𝑀 ‘ ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∪ 𝑏 ) ) )
35		fveq2	⊢ ( 𝑎 = ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) → ( 𝑀 ‘ 𝑎 ) = ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) )
36	35	oveq1d	⊢ ( 𝑎 = ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) → ( ( 𝑀 ‘ 𝑎 ) +e ( 𝑀 ‘ 𝑏 ) ) = ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ 𝑏 ) ) )
37	34 36	breq12d	⊢ ( 𝑎 = ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) → ( ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +e ( 𝑀 ‘ 𝑏 ) ) ↔ ( 𝑀 ‘ ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ 𝑏 ) ) ) )
38		uneq2	⊢ ( 𝑏 = ( 𝑒 ∖ 𝐴 ) → ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∪ 𝑏 ) = ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∪ ( 𝑒 ∖ 𝐴 ) ) )
39	38	fveq2d	⊢ ( 𝑏 = ( 𝑒 ∖ 𝐴 ) → ( 𝑀 ‘ ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∪ 𝑏 ) ) = ( 𝑀 ‘ ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∪ ( 𝑒 ∖ 𝐴 ) ) ) )
40		fveq2	⊢ ( 𝑏 = ( 𝑒 ∖ 𝐴 ) → ( 𝑀 ‘ 𝑏 ) = ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) )
41	40	oveq2d	⊢ ( 𝑏 = ( 𝑒 ∖ 𝐴 ) → ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ 𝑏 ) ) = ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) )
42	39 41	breq12d	⊢ ( 𝑏 = ( 𝑒 ∖ 𝐴 ) → ( ( 𝑀 ‘ ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ 𝑏 ) ) ↔ ( 𝑀 ‘ ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∪ ( 𝑒 ∖ 𝐴 ) ) ) ≤ ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) ) )
43	37 42	rspc2v	⊢ ( ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∈ 𝒫 𝑂 ∧ ( 𝑒 ∖ 𝐴 ) ∈ 𝒫 𝑂 ) → ( ∀ 𝑎 ∈ 𝒫 𝑂 ∀ 𝑏 ∈ 𝒫 𝑂 ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +e ( 𝑀 ‘ 𝑏 ) ) → ( 𝑀 ‘ ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∪ ( 𝑒 ∖ 𝐴 ) ) ) ≤ ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) ) )
44	43	imp	⊢ ( ( ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∈ 𝒫 𝑂 ∧ ( 𝑒 ∖ 𝐴 ) ∈ 𝒫 𝑂 ) ∧ ∀ 𝑎 ∈ 𝒫 𝑂 ∀ 𝑏 ∈ 𝒫 𝑂 ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +e ( 𝑀 ‘ 𝑏 ) ) ) → ( 𝑀 ‘ ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∪ ( 𝑒 ∖ 𝐴 ) ) ) ≤ ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) )
45	18 21 32 44	syl21anc	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ∪ ( 𝑒 ∖ 𝐴 ) ) ) ≤ ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) )
46	29 45	eqbrtrrid	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ≤ ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) )
47		xleadd2a	⊢ ( ( ( ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∈ ℝ* ∧ ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) ∈ ℝ* ∧ ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) ∈ ℝ* ) ∧ ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ≤ ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) ) )
48	16 24 27 46 47	syl31anc	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) ) )
49	1 2	elcarsg	⊢ ( 𝜑 → ( 𝐵 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( 𝐵 ⊆ 𝑂 ∧ ∀ 𝑓 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑓 ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑓 ∖ 𝐵 ) ) ) = ( 𝑀 ‘ 𝑓 ) ) ) )
50	5 49	mpbid	⊢ ( 𝜑 → ( 𝐵 ⊆ 𝑂 ∧ ∀ 𝑓 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑓 ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑓 ∖ 𝐵 ) ) ) = ( 𝑀 ‘ 𝑓 ) ) )
51	50	simprd	⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑓 ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑓 ∖ 𝐵 ) ) ) = ( 𝑀 ‘ 𝑓 ) )
52	51	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ∀ 𝑓 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑓 ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑓 ∖ 𝐵 ) ) ) = ( 𝑀 ‘ 𝑓 ) )
53		ineq1	⊢ ( 𝑓 = ( 𝑒 ∩ 𝐴 ) → ( 𝑓 ∩ 𝐵 ) = ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) )
54	53	fveq2d	⊢ ( 𝑓 = ( 𝑒 ∩ 𝐴 ) → ( 𝑀 ‘ ( 𝑓 ∩ 𝐵 ) ) = ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) )
55		difeq1	⊢ ( 𝑓 = ( 𝑒 ∩ 𝐴 ) → ( 𝑓 ∖ 𝐵 ) = ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) )
56	55	fveq2d	⊢ ( 𝑓 = ( 𝑒 ∩ 𝐴 ) → ( 𝑀 ‘ ( 𝑓 ∖ 𝐵 ) ) = ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) )
57	54 56	oveq12d	⊢ ( 𝑓 = ( 𝑒 ∩ 𝐴 ) → ( ( 𝑀 ‘ ( 𝑓 ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑓 ∖ 𝐵 ) ) ) = ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) ) )
58		fveq2	⊢ ( 𝑓 = ( 𝑒 ∩ 𝐴 ) → ( 𝑀 ‘ 𝑓 ) = ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) )
59	57 58	eqeq12d	⊢ ( 𝑓 = ( 𝑒 ∩ 𝐴 ) → ( ( ( 𝑀 ‘ ( 𝑓 ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑓 ∖ 𝐵 ) ) ) = ( 𝑀 ‘ 𝑓 ) ↔ ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) ) = ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) ) )
60	59	adantl	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) ∧ 𝑓 = ( 𝑒 ∩ 𝐴 ) ) → ( ( ( 𝑀 ‘ ( 𝑓 ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑓 ∖ 𝐵 ) ) ) = ( 𝑀 ‘ 𝑓 ) ↔ ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) ) = ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) ) )
61	17 60	rspcdv	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ∀ 𝑓 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑓 ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑓 ∖ 𝐵 ) ) ) = ( 𝑀 ‘ 𝑓 ) → ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) ) = ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) ) )
62	52 61	mpd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) ) = ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) )
63	62	oveq1d	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) )
64	17	elpwincl1	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ∈ 𝒫 𝑂 )
65	12 64	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
66		xrge0addass	⊢ ( ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ∈ ( 0 [,] +∞ ) ) → ( ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) +e ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) ) )
67	65 19 22 66	syl3anc	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) +e ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) ) )
68		inass	⊢ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) = ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) )
69	68	fveq2i	⊢ ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) = ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) )
70	69	oveq1i	⊢ ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) +e ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) ) = ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) )
71	67 70	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∩ 𝐵 ) ) +e ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) ) )
72	7	simprd	⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) )
73	72	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) )
74	63 71 73	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( ( 𝑀 ‘ ( ( 𝑒 ∩ 𝐴 ) ∖ 𝐵 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) ) = ( 𝑀 ‘ 𝑒 ) )
75	48 74	breqtrd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ≤ ( 𝑀 ‘ 𝑒 ) )
76		inundif	⊢ ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) = 𝑒
77	76	fveq2i	⊢ ( 𝑀 ‘ ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) = ( 𝑀 ‘ 𝑒 )
78		uneq1	⊢ ( 𝑎 = ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) → ( 𝑎 ∪ 𝑏 ) = ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∪ 𝑏 ) )
79	78	fveq2d	⊢ ( 𝑎 = ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) → ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) = ( 𝑀 ‘ ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∪ 𝑏 ) ) )
80		fveq2	⊢ ( 𝑎 = ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) → ( 𝑀 ‘ 𝑎 ) = ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) )
81	80	oveq1d	⊢ ( 𝑎 = ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑀 ‘ 𝑎 ) +e ( 𝑀 ‘ 𝑏 ) ) = ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ 𝑏 ) ) )
82	79 81	breq12d	⊢ ( 𝑎 = ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +e ( 𝑀 ‘ 𝑏 ) ) ↔ ( 𝑀 ‘ ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ 𝑏 ) ) ) )
83		uneq2	⊢ ( 𝑏 = ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∪ 𝑏 ) = ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) )
84	83	fveq2d	⊢ ( 𝑏 = ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) → ( 𝑀 ‘ ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∪ 𝑏 ) ) = ( 𝑀 ‘ ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) )
85		fveq2	⊢ ( 𝑏 = ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) → ( 𝑀 ‘ 𝑏 ) = ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) )
86	85	oveq2d	⊢ ( 𝑏 = ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ 𝑏 ) ) = ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) )
87	84 86	breq12d	⊢ ( 𝑏 = ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑀 ‘ ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ 𝑏 ) ) ↔ ( 𝑀 ‘ ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ) )
88	82 87	rspc2v	⊢ ( ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∈ 𝒫 𝑂 ∧ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ∈ 𝒫 𝑂 ) → ( ∀ 𝑎 ∈ 𝒫 𝑂 ∀ 𝑏 ∈ 𝒫 𝑂 ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +e ( 𝑀 ‘ 𝑏 ) ) → ( 𝑀 ‘ ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ) )
89	88	imp	⊢ ( ( ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∈ 𝒫 𝑂 ∧ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ∈ 𝒫 𝑂 ) ∧ ∀ 𝑎 ∈ 𝒫 𝑂 ∀ 𝑏 ∈ 𝒫 𝑂 ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +e ( 𝑀 ‘ 𝑏 ) ) ) → ( 𝑀 ‘ ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) )
90	25 14 32 89	syl21anc	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) )
91	77 90	eqbrtrrid	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑒 ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) )
92	75 91	jca	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ≤ ( 𝑀 ‘ 𝑒 ) ∧ ( 𝑀 ‘ 𝑒 ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ) )
93	27 16	xaddcld	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ∈ ℝ* )
94	2	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑒 ) ∈ ( 0 [,] +∞ ) )
95	11 94	sselid	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑒 ) ∈ ℝ* )
96		xrletri3	⊢ ( ( ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ∈ ℝ* ∧ ( 𝑀 ‘ 𝑒 ) ∈ ℝ* ) → ( ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) = ( 𝑀 ‘ 𝑒 ) ↔ ( ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ≤ ( 𝑀 ‘ 𝑒 ) ∧ ( 𝑀 ‘ 𝑒 ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ) ) )
97	93 95 96	syl2anc	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) = ( 𝑀 ‘ 𝑒 ) ↔ ( ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ≤ ( 𝑀 ‘ 𝑒 ) ∧ ( 𝑀 ‘ 𝑒 ) ≤ ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) ) ) )
98	92 97	mpbird	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) = ( 𝑀 ‘ 𝑒 ) )
99	98	ralrimiva	⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) = ( 𝑀 ‘ 𝑒 ) )
100	10 99	jca	⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) = ( 𝑀 ‘ 𝑒 ) ) )
101	1 2	elcarsg	⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝐴 ∩ 𝐵 ) ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ( 𝐴 ∩ 𝐵 ) ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )
102	100 101	mpbird	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ ( toCaraSiga ‘ 𝑀 ) )