carsgclctunlem2

	Ref	Expression
Hypotheses	carsgval.1	$⊢ φ \to O \in V$
	carsgval.2	$⊢ φ \to M : 𝒫 O ⟶ [0, +∞]$
	carsgsiga.1	$⊢ φ \to M (\emptyset) = 0$
	carsgsiga.2	$⊢ (φ \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
	carsgsiga.3	$⊢ (φ \land x \subseteq y \land y \in 𝒫 O) \to M (x) \leq M (y)$
	carsgclctunlem2.1	$⊢ φ \to \underset{k \in ℕ}{Disj} A$
	carsgclctunlem2.2	$⊢ (φ \land k \in ℕ) \to A \in toCaraSiga (M)$
	carsgclctunlem2.3	$⊢ φ \to E \in 𝒫 O$
	carsgclctunlem2.4	$⊢ φ \to M (E) \neq +∞$
Assertion	carsgclctunlem2	$⊢ φ \to M (E \cap ⋃_{k \in ℕ} A) +_{𝑒} M (E ∖ ⋃_{k \in ℕ} A) \leq M (E)$

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	$⊢ φ \to O \in V$
2		carsgval.2	$⊢ φ \to M : 𝒫 O ⟶ [0, +∞]$
3		carsgsiga.1	$⊢ φ \to M (\emptyset) = 0$
4		carsgsiga.2	$⊢ (φ \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
5		carsgsiga.3	$⊢ (φ \land x \subseteq y \land y \in 𝒫 O) \to M (x) \leq M (y)$
6		carsgclctunlem2.1	$⊢ φ \to \underset{k \in ℕ}{Disj} A$
7		carsgclctunlem2.2	$⊢ (φ \land k \in ℕ) \to A \in toCaraSiga (M)$
8		carsgclctunlem2.3	$⊢ φ \to E \in 𝒫 O$
9		carsgclctunlem2.4	$⊢ φ \to M (E) \neq +∞$
10		iunin2	$⊢ ⋃_{k \in ℕ} (E \cap A) = E \cap ⋃_{k \in ℕ} A$
11	10	fveq2i	$⊢ M (⋃_{k \in ℕ} (E \cap A)) = M (E \cap ⋃_{k \in ℕ} A)$
12		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
13		nnex	$⊢ ℕ \in V$
14	13	a1i	$⊢ φ \to ℕ \in V$
15	8	adantr	$⊢ (φ \land k \in ℕ) \to E \in 𝒫 O$
16	15	elpwincl1	$⊢ (φ \land k \in ℕ) \to E \cap A \in 𝒫 O$
17	14 16	elpwiuncl	$⊢ φ \to ⋃_{k \in ℕ} (E \cap A) \in 𝒫 O$
18	2 17	ffvelcdmd	$⊢ φ \to M (⋃_{k \in ℕ} (E \cap A)) \in [0, +∞]$
19	12 18	sselid	$⊢ φ \to M (⋃_{k \in ℕ} (E \cap A)) \in ℝ^{*}$
20	11 19	eqeltrrid	$⊢ φ \to M (E \cap ⋃_{k \in ℕ} A) \in ℝ^{*}$
21	2 8	ffvelcdmd	$⊢ φ \to M (E) \in [0, +∞]$
22	12 21	sselid	$⊢ φ \to M (E) \in ℝ^{*}$
23	8	elpwdifcl	$⊢ φ \to E ∖ ⋃_{k \in ℕ} A \in 𝒫 O$
24	2 23	ffvelcdmd	$⊢ φ \to M (E ∖ ⋃_{k \in ℕ} A) \in [0, +∞]$
25	12 24	sselid	$⊢ φ \to M (E ∖ ⋃_{k \in ℕ} A) \in ℝ^{*}$
26	25	xnegcld	$⊢ φ \to - M (E ∖ ⋃_{k \in ℕ} A) \in ℝ^{*}$
27	22 26	xaddcld	$⊢ φ \to M (E) +_{𝑒} (- M (E ∖ ⋃_{k \in ℕ} A)) \in ℝ^{*}$
28	2	adantr	$⊢ (φ \land k \in ℕ) \to M : 𝒫 O ⟶ [0, +∞]$
29	28 16	ffvelcdmd	$⊢ (φ \land k \in ℕ) \to M (E \cap A) \in [0, +∞]$
30	29	ralrimiva	$⊢ φ \to \forall k \in ℕ M (E \cap A) \in [0, +∞]$
31		nfcv	$⊢ \underline{Ⅎ} k ℕ$
32	31	esumcl	$⊢ (ℕ \in V \land \forall k \in ℕ M (E \cap A) \in [0, +∞]) \to \underset{k \in ℕ}{\sum^{*}} M (E \cap A) \in [0, +∞]$
33	14 30 32	syl2anc	$⊢ φ \to \underset{k \in ℕ}{\sum^{*}} M (E \cap A) \in [0, +∞]$
34	12 33	sselid	$⊢ φ \to \underset{k \in ℕ}{\sum^{}} M (E \cap A) \in ℝ^{}$
35	16	ralrimiva	$⊢ φ \to \forall k \in ℕ E \cap A \in 𝒫 O$
36		dfiun3g	$⊢ \forall k \in ℕ E \cap A \in 𝒫 O \to ⋃_{k \in ℕ} (E \cap A) = ⋃ ran (k \in ℕ ⟼ E \cap A)$
37	35 36	syl	$⊢ φ \to ⋃_{k \in ℕ} (E \cap A) = ⋃ ran (k \in ℕ ⟼ E \cap A)$
38	37	fveq2d	$⊢ φ \to M (⋃_{k \in ℕ} (E \cap A)) = M (⋃ ran (k \in ℕ ⟼ E \cap A))$
39		nnct	$⊢ ℕ ≼ ω$
40		mptct	$⊢ ℕ ≼ ω \to (k \in ℕ ⟼ E \cap A) ≼ ω$
41		rnct	$⊢ (k \in ℕ ⟼ E \cap A) ≼ ω \to ran (k \in ℕ ⟼ E \cap A) ≼ ω$
42	39 40 41	mp2b	$⊢ ran (k \in ℕ ⟼ E \cap A) ≼ ω$
43	42	a1i	$⊢ φ \to ran (k \in ℕ ⟼ E \cap A) ≼ ω$
44		eqid	$⊢ (k \in ℕ ⟼ E \cap A) = (k \in ℕ ⟼ E \cap A)$
45	44	rnmptss	$⊢ \forall k \in ℕ E \cap A \in 𝒫 O \to ran (k \in ℕ ⟼ E \cap A) \subseteq 𝒫 O$
46	35 45	syl	$⊢ φ \to ran (k \in ℕ ⟼ E \cap A) \subseteq 𝒫 O$
47		mptexg	$⊢ ℕ \in V \to (k \in ℕ ⟼ E \cap A) \in V$
48		rnexg	$⊢ (k \in ℕ ⟼ E \cap A) \in V \to ran (k \in ℕ ⟼ E \cap A) \in V$
49	13 47 48	mp2b	$⊢ ran (k \in ℕ ⟼ E \cap A) \in V$
50		breq1	$⊢ x = ran (k \in ℕ ⟼ E \cap A) \to (x ≼ ω \leftrightarrow ran (k \in ℕ ⟼ E \cap A) ≼ ω)$
51		sseq1	$⊢ x = ran (k \in ℕ ⟼ E \cap A) \to (x \subseteq 𝒫 O \leftrightarrow ran (k \in ℕ ⟼ E \cap A) \subseteq 𝒫 O)$
52	50 51	3anbi23d	$⊢ x = ran (k \in ℕ ⟼ E \cap A) \to ((φ \land x ≼ ω \land x \subseteq 𝒫 O) \leftrightarrow (φ \land ran (k \in ℕ ⟼ E \cap A) ≼ ω \land ran (k \in ℕ ⟼ E \cap A) \subseteq 𝒫 O))$
53		unieq	$⊢ x = ran (k \in ℕ ⟼ E \cap A) \to ⋃ x = ⋃ ran (k \in ℕ ⟼ E \cap A)$
54	53	fveq2d	$⊢ x = ran (k \in ℕ ⟼ E \cap A) \to M (⋃ x) = M (⋃ ran (k \in ℕ ⟼ E \cap A))$
55		esumeq1	$⊢ x = ran (k \in ℕ ⟼ E \cap A) \to \underset{y \in x}{\sum^{}} M (y) = \underset{y \in ran (k \in ℕ ⟼ E \cap A)}{\sum^{}} M (y)$
56	54 55	breq12d	$⊢ x = ran (k \in ℕ ⟼ E \cap A) \to (M (⋃ x) \leq \underset{y \in x}{\sum^{}} M (y) \leftrightarrow M (⋃ ran (k \in ℕ ⟼ E \cap A)) \leq \underset{y \in ran (k \in ℕ ⟼ E \cap A)}{\sum^{}} M (y))$
57	52 56	imbi12d	$⊢ x = ran (k \in ℕ ⟼ E \cap A) \to (((φ \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{}} M (y)) \leftrightarrow ((φ \land ran (k \in ℕ ⟼ E \cap A) ≼ ω \land ran (k \in ℕ ⟼ E \cap A) \subseteq 𝒫 O) \to M (⋃ ran (k \in ℕ ⟼ E \cap A)) \leq \underset{y \in ran (k \in ℕ ⟼ E \cap A)}{\sum^{}} M (y)))$
58	57 4	vtoclg	$⊢ ran (k \in ℕ ⟼ E \cap A) \in V \to ((φ \land ran (k \in ℕ ⟼ E \cap A) ≼ ω \land ran (k \in ℕ ⟼ E \cap A) \subseteq 𝒫 O) \to M (⋃ ran (k \in ℕ ⟼ E \cap A)) \leq \underset{y \in ran (k \in ℕ ⟼ E \cap A)}{\sum^{*}} M (y))$
59	49 58	ax-mp	$⊢ (φ \land ran (k \in ℕ ⟼ E \cap A) ≼ ω \land ran (k \in ℕ ⟼ E \cap A) \subseteq 𝒫 O) \to M (⋃ ran (k \in ℕ ⟼ E \cap A)) \leq \underset{y \in ran (k \in ℕ ⟼ E \cap A)}{\sum^{*}} M (y)$
60	43 46 59	mpd3an23	$⊢ φ \to M (⋃ ran (k \in ℕ ⟼ E \cap A)) \leq \underset{y \in ran (k \in ℕ ⟼ E \cap A)}{\sum^{*}} M (y)$
61	38 60	eqbrtrd	$⊢ φ \to M (⋃_{k \in ℕ} (E \cap A)) \leq \underset{y \in ran (k \in ℕ ⟼ E \cap A)}{\sum^{*}} M (y)$
62		fveq2	$⊢ y = E \cap A \to M (y) = M (E \cap A)$
63		simpr	$⊢ ((φ \land k \in ℕ) \land E \cap A = \emptyset) \to E \cap A = \emptyset$
64	63	fveq2d	$⊢ ((φ \land k \in ℕ) \land E \cap A = \emptyset) \to M (E \cap A) = M (\emptyset)$
65	3	ad2antrr	$⊢ ((φ \land k \in ℕ) \land E \cap A = \emptyset) \to M (\emptyset) = 0$
66	64 65	eqtrd	$⊢ ((φ \land k \in ℕ) \land E \cap A = \emptyset) \to M (E \cap A) = 0$
67		disjin	$⊢ \underset{k \in ℕ}{Disj} A \to \underset{k \in ℕ}{Disj} (A \cap E)$
68	6 67	syl	$⊢ φ \to \underset{k \in ℕ}{Disj} (A \cap E)$
69		incom	$⊢ A \cap E = E \cap A$
70	69	rgenw	$⊢ \forall k \in ℕ A \cap E = E \cap A$
71		disjeq2	$⊢ \forall k \in ℕ A \cap E = E \cap A \to (\underset{k \in ℕ}{Disj} (A \cap E) \leftrightarrow \underset{k \in ℕ}{Disj} (E \cap A))$
72	70 71	ax-mp	$⊢ \underset{k \in ℕ}{Disj} (A \cap E) \leftrightarrow \underset{k \in ℕ}{Disj} (E \cap A)$
73	68 72	sylib	$⊢ φ \to \underset{k \in ℕ}{Disj} (E \cap A)$
74	62 14 29 16 66 73	esumrnmpt2	$⊢ φ \to \underset{y \in ran (k \in ℕ ⟼ E \cap A)}{\sum^{}} M (y) = \underset{k \in ℕ}{\sum^{}} M (E \cap A)$
75	61 74	breqtrd	$⊢ φ \to M (⋃_{k \in ℕ} (E \cap A)) \leq \underset{k \in ℕ}{\sum^{*}} M (E \cap A)$
76		difssd	$⊢ φ \to E ∖ ⋃_{k \in ℕ} A \subseteq E$
77	1 2 76 8 5	carsgmon	$⊢ φ \to M (E ∖ ⋃_{k \in ℕ} A) \leq M (E)$
78	21 24 77	xrge0subcld	$⊢ φ \to M (E) +_{𝑒} (- M (E ∖ ⋃_{k \in ℕ} A)) \in [0, +∞]$
79	2	adantr	$⊢ (φ \land n \in ℕ) \to M : 𝒫 O ⟶ [0, +∞]$
80	8	adantr	$⊢ (φ \land n \in ℕ) \to E \in 𝒫 O$
81	80	elpwincl1	$⊢ (φ \land n \in ℕ) \to E \cap ⋃_{k = 1}^{n} A \in 𝒫 O$
82	79 81	ffvelcdmd	$⊢ (φ \land n \in ℕ) \to M (E \cap ⋃_{k = 1}^{n} A) \in [0, +∞]$
83	12 82	sselid	$⊢ (φ \land n \in ℕ) \to M (E \cap ⋃_{k = 1}^{n} A) \in ℝ^{*}$
84		xrge0neqmnf	$⊢ M (E \cap ⋃_{k = 1}^{n} A) \in [0, +∞] \to M (E \cap ⋃_{k = 1}^{n} A) \neq −∞$
85	82 84	syl	$⊢ (φ \land n \in ℕ) \to M (E \cap ⋃_{k = 1}^{n} A) \neq −∞$
86	80	elpwdifcl	$⊢ (φ \land n \in ℕ) \to E ∖ ⋃_{k = 1}^{n} A \in 𝒫 O$
87	79 86	ffvelcdmd	$⊢ (φ \land n \in ℕ) \to M (E ∖ ⋃_{k = 1}^{n} A) \in [0, +∞]$
88	12 87	sselid	$⊢ (φ \land n \in ℕ) \to M (E ∖ ⋃_{k = 1}^{n} A) \in ℝ^{*}$
89		xrge0neqmnf	$⊢ M (E ∖ ⋃_{k = 1}^{n} A) \in [0, +∞] \to M (E ∖ ⋃_{k = 1}^{n} A) \neq −∞$
90	87 89	syl	$⊢ (φ \land n \in ℕ) \to M (E ∖ ⋃_{k = 1}^{n} A) \neq −∞$
91	88	xnegcld	$⊢ (φ \land n \in ℕ) \to - M (E ∖ ⋃_{k = 1}^{n} A) \in ℝ^{*}$
92		xnegneg	$⊢ M (E ∖ ⋃_{k = 1}^{n} A) \in ℝ^{*} \to - (- M (E ∖ ⋃_{k = 1}^{n} A)) = M (E ∖ ⋃_{k = 1}^{n} A)$
93	88 92	syl	$⊢ (φ \land n \in ℕ) \to - (- M (E ∖ ⋃_{k = 1}^{n} A)) = M (E ∖ ⋃_{k = 1}^{n} A)$
94	93	adantr	$⊢ ((φ \land n \in ℕ) \land - M (E ∖ ⋃_{k = 1}^{n} A) = −∞) \to - (- M (E ∖ ⋃_{k = 1}^{n} A)) = M (E ∖ ⋃_{k = 1}^{n} A)$
95		xnegeq	$⊢ - M (E ∖ ⋃_{k = 1}^{n} A) = −∞ \to - (- M (E ∖ ⋃_{k = 1}^{n} A)) = - −∞$
96	95	adantl	$⊢ ((φ \land n \in ℕ) \land - M (E ∖ ⋃_{k = 1}^{n} A) = −∞) \to - (- M (E ∖ ⋃_{k = 1}^{n} A)) = - −∞$
97		xnegmnf	$⊢ - −∞ = +∞$
98	96 97	eqtrdi	$⊢ ((φ \land n \in ℕ) \land - M (E ∖ ⋃_{k = 1}^{n} A) = −∞) \to - (- M (E ∖ ⋃_{k = 1}^{n} A)) = +∞$
99	94 98	eqtr3d	$⊢ ((φ \land n \in ℕ) \land - M (E ∖ ⋃_{k = 1}^{n} A) = −∞) \to M (E ∖ ⋃_{k = 1}^{n} A) = +∞$
100	99	oveq2d	$⊢ ((φ \land n \in ℕ) \land - M (E ∖ ⋃_{k = 1}^{n} A) = −∞) \to M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (E ∖ ⋃_{k = 1}^{n} A) = M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} +∞$
101		simpll	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to φ$
102		fz1ssnn	$⊢ (1 \dots n) \subseteq ℕ$
103	102	a1i	$⊢ (φ \land n \in ℕ) \to (1 \dots n) \subseteq ℕ$
104	103	sselda	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k \in ℕ$
105	101 104 7	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A \in toCaraSiga (M)$
106	105	ralrimiva	$⊢ (φ \land n \in ℕ) \to \forall k \in (1 \dots n) A \in toCaraSiga (M)$
107		dfiun3g	$⊢ \forall k \in (1 \dots n) A \in toCaraSiga (M) \to ⋃_{k = 1}^{n} A = ⋃ ran (k \in (1 \dots n) ⟼ A)$
108	106 107	syl	$⊢ (φ \land n \in ℕ) \to ⋃_{k = 1}^{n} A = ⋃ ran (k \in (1 \dots n) ⟼ A)$
109	1	adantr	$⊢ (φ \land n \in ℕ) \to O \in V$
110	3	adantr	$⊢ (φ \land n \in ℕ) \to M (\emptyset) = 0$
111	4	3adant1r	$⊢ ((φ \land n \in ℕ) \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
112		fzfi	$⊢ (1 \dots n) \in Fin$
113		mptfi	$⊢ (1 \dots n) \in Fin \to (k \in (1 \dots n) ⟼ A) \in Fin$
114		rnfi	$⊢ (k \in (1 \dots n) ⟼ A) \in Fin \to ran (k \in (1 \dots n) ⟼ A) \in Fin$
115	112 113 114	mp2b	$⊢ ran (k \in (1 \dots n) ⟼ A) \in Fin$
116	115	a1i	$⊢ (φ \land n \in ℕ) \to ran (k \in (1 \dots n) ⟼ A) \in Fin$
117		eqid	$⊢ (k \in (1 \dots n) ⟼ A) = (k \in (1 \dots n) ⟼ A)$
118	117	rnmptss	$⊢ \forall k \in (1 \dots n) A \in toCaraSiga (M) \to ran (k \in (1 \dots n) ⟼ A) \subseteq toCaraSiga (M)$
119	106 118	syl	$⊢ (φ \land n \in ℕ) \to ran (k \in (1 \dots n) ⟼ A) \subseteq toCaraSiga (M)$
120	109 79 110 111 116 119	fiunelcarsg	$⊢ (φ \land n \in ℕ) \to ⋃ ran (k \in (1 \dots n) ⟼ A) \in toCaraSiga (M)$
121	108 120	eqeltrd	$⊢ (φ \land n \in ℕ) \to ⋃_{k = 1}^{n} A \in toCaraSiga (M)$
122	109 79	elcarsg	$⊢ (φ \land n \in ℕ) \to (⋃_{k = 1}^{n} A \in toCaraSiga (M) \leftrightarrow (⋃_{k = 1}^{n} A \subseteq O \land \forall e \in 𝒫 O M (e \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (e ∖ ⋃_{k = 1}^{n} A) = M (e)))$
123	121 122	mpbid	$⊢ (φ \land n \in ℕ) \to (⋃_{k = 1}^{n} A \subseteq O \land \forall e \in 𝒫 O M (e \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (e ∖ ⋃_{k = 1}^{n} A) = M (e))$
124	123	simprd	$⊢ (φ \land n \in ℕ) \to \forall e \in 𝒫 O M (e \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (e ∖ ⋃_{k = 1}^{n} A) = M (e)$
125		ineq1	$⊢ e = E \to e \cap ⋃_{k = 1}^{n} A = E \cap ⋃_{k = 1}^{n} A$
126	125	fveq2d	$⊢ e = E \to M (e \cap ⋃_{k = 1}^{n} A) = M (E \cap ⋃_{k = 1}^{n} A)$
127		difeq1	$⊢ e = E \to e ∖ ⋃_{k = 1}^{n} A = E ∖ ⋃_{k = 1}^{n} A$
128	127	fveq2d	$⊢ e = E \to M (e ∖ ⋃_{k = 1}^{n} A) = M (E ∖ ⋃_{k = 1}^{n} A)$
129	126 128	oveq12d	$⊢ e = E \to M (e \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (e ∖ ⋃_{k = 1}^{n} A) = M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (E ∖ ⋃_{k = 1}^{n} A)$
130		fveq2	$⊢ e = E \to M (e) = M (E)$
131	129 130	eqeq12d	$⊢ e = E \to (M (e \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (e ∖ ⋃_{k = 1}^{n} A) = M (e) \leftrightarrow M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (E ∖ ⋃_{k = 1}^{n} A) = M (E))$
132	131	rspcv	$⊢ E \in 𝒫 O \to (\forall e \in 𝒫 O M (e \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (e ∖ ⋃_{k = 1}^{n} A) = M (e) \to M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (E ∖ ⋃_{k = 1}^{n} A) = M (E))$
133	80 124 132	sylc	$⊢ (φ \land n \in ℕ) \to M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (E ∖ ⋃_{k = 1}^{n} A) = M (E)$
134	133	adantr	$⊢ ((φ \land n \in ℕ) \land - M (E ∖ ⋃_{k = 1}^{n} A) = −∞) \to M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (E ∖ ⋃_{k = 1}^{n} A) = M (E)$
135		xaddpnf1	$⊢ (M (E \cap ⋃_{k = 1}^{n} A) \in ℝ^{*} \land M (E \cap ⋃_{k = 1}^{n} A) \neq −∞) \to M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} +∞ = +∞$
136	83 85 135	syl2anc	$⊢ (φ \land n \in ℕ) \to M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} +∞ = +∞$
137	136	adantr	$⊢ ((φ \land n \in ℕ) \land - M (E ∖ ⋃_{k = 1}^{n} A) = −∞) \to M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} +∞ = +∞$
138	100 134 137	3eqtr3d	$⊢ ((φ \land n \in ℕ) \land - M (E ∖ ⋃_{k = 1}^{n} A) = −∞) \to M (E) = +∞$
139	9	ad2antrr	$⊢ ((φ \land n \in ℕ) \land - M (E ∖ ⋃_{k = 1}^{n} A) = −∞) \to M (E) \neq +∞$
140	139	neneqd	$⊢ ((φ \land n \in ℕ) \land - M (E ∖ ⋃_{k = 1}^{n} A) = −∞) \to \neg M (E) = +∞$
141	138 140	pm2.65da	$⊢ (φ \land n \in ℕ) \to \neg - M (E ∖ ⋃_{k = 1}^{n} A) = −∞$
142	141	neqned	$⊢ (φ \land n \in ℕ) \to - M (E ∖ ⋃_{k = 1}^{n} A) \neq −∞$
143		xaddass	$⊢ ((M (E \cap ⋃_{k = 1}^{n} A) \in ℝ^{} \land M (E \cap ⋃_{k = 1}^{n} A) \neq −∞) \land (M (E ∖ ⋃_{k = 1}^{n} A) \in ℝ^{} \land M (E ∖ ⋃_{k = 1}^{n} A) \neq −∞) \land (- M (E ∖ ⋃_{k = 1}^{n} A) \in ℝ^{*} \land - M (E ∖ ⋃_{k = 1}^{n} A) \neq −∞)) \to (M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (E ∖ ⋃_{k = 1}^{n} A)) +_{𝑒} (- M (E ∖ ⋃_{k = 1}^{n} A)) = M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} (M (E ∖ ⋃_{k = 1}^{n} A) +_{𝑒} (- M (E ∖ ⋃_{k = 1}^{n} A)))$
144	83 85 88 90 91 142 143	syl222anc	$⊢ (φ \land n \in ℕ) \to (M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (E ∖ ⋃_{k = 1}^{n} A)) +_{𝑒} (- M (E ∖ ⋃_{k = 1}^{n} A)) = M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} (M (E ∖ ⋃_{k = 1}^{n} A) +_{𝑒} (- M (E ∖ ⋃_{k = 1}^{n} A)))$
145		xnegid	$⊢ M (E ∖ ⋃_{k = 1}^{n} A) \in ℝ^{*} \to M (E ∖ ⋃_{k = 1}^{n} A) +_{𝑒} (- M (E ∖ ⋃_{k = 1}^{n} A)) = 0$
146	88 145	syl	$⊢ (φ \land n \in ℕ) \to M (E ∖ ⋃_{k = 1}^{n} A) +_{𝑒} (- M (E ∖ ⋃_{k = 1}^{n} A)) = 0$
147	146	oveq2d	$⊢ (φ \land n \in ℕ) \to M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} (M (E ∖ ⋃_{k = 1}^{n} A) +_{𝑒} (- M (E ∖ ⋃_{k = 1}^{n} A))) = M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} 0$
148		xaddrid	$⊢ M (E \cap ⋃_{k = 1}^{n} A) \in ℝ^{*} \to M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} 0 = M (E \cap ⋃_{k = 1}^{n} A)$
149	83 148	syl	$⊢ (φ \land n \in ℕ) \to M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} 0 = M (E \cap ⋃_{k = 1}^{n} A)$
150	144 147 149	3eqtrd	$⊢ (φ \land n \in ℕ) \to (M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (E ∖ ⋃_{k = 1}^{n} A)) +_{𝑒} (- M (E ∖ ⋃_{k = 1}^{n} A)) = M (E \cap ⋃_{k = 1}^{n} A)$
151	133	oveq1d	$⊢ (φ \land n \in ℕ) \to (M (E \cap ⋃_{k = 1}^{n} A) +_{𝑒} M (E ∖ ⋃_{k = 1}^{n} A)) +_{𝑒} (- M (E ∖ ⋃_{k = 1}^{n} A)) = M (E) +_{𝑒} (- M (E ∖ ⋃_{k = 1}^{n} A))$
152	108	ineq2d	$⊢ (φ \land n \in ℕ) \to E \cap ⋃_{k = 1}^{n} A = E \cap ⋃ ran (k \in (1 \dots n) ⟼ A)$
153	152	fveq2d	$⊢ (φ \land n \in ℕ) \to M (E \cap ⋃_{k = 1}^{n} A) = M (E \cap ⋃ ran (k \in (1 \dots n) ⟼ A))$
154		mptss	$⊢ (1 \dots n) \subseteq ℕ \to (k \in (1 \dots n) ⟼ A) \subseteq (k \in ℕ ⟼ A)$
155		rnss	$⊢ (k \in (1 \dots n) ⟼ A) \subseteq (k \in ℕ ⟼ A) \to ran (k \in (1 \dots n) ⟼ A) \subseteq ran (k \in ℕ ⟼ A)$
156	102 154 155	mp2b	$⊢ ran (k \in (1 \dots n) ⟼ A) \subseteq ran (k \in ℕ ⟼ A)$
157	156	a1i	$⊢ (φ \land n \in ℕ) \to ran (k \in (1 \dots n) ⟼ A) \subseteq ran (k \in ℕ ⟼ A)$
158		disjrnmpt	$⊢ \underset{k \in ℕ}{Disj} A \to \underset{y \in ran (k \in ℕ ⟼ A)}{Disj} y$
159	6 158	syl	$⊢ φ \to \underset{y \in ran (k \in ℕ ⟼ A)}{Disj} y$
160	159	adantr	$⊢ (φ \land n \in ℕ) \to \underset{y \in ran (k \in ℕ ⟼ A)}{Disj} y$
161		disjss1	$⊢ ran (k \in (1 \dots n) ⟼ A) \subseteq ran (k \in ℕ ⟼ A) \to (\underset{y \in ran (k \in ℕ ⟼ A)}{Disj} y \to \underset{y \in ran (k \in (1 \dots n) ⟼ A)}{Disj} y)$
162	157 160 161	sylc	$⊢ (φ \land n \in ℕ) \to \underset{y \in ran (k \in (1 \dots n) ⟼ A)}{Disj} y$
163	109 79 110 111 116 119 162 80	carsgclctunlem1	$⊢ (φ \land n \in ℕ) \to M (E \cap ⋃ ran (k \in (1 \dots n) ⟼ A)) = \underset{y \in ran (k \in (1 \dots n) ⟼ A)}{\sum^{*}} M (E \cap y)$
164		ineq2	$⊢ y = A \to E \cap y = E \cap A$
165	164	fveq2d	$⊢ y = A \to M (E \cap y) = M (E \cap A)$
166	112	elexi	$⊢ (1 \dots n) \in V$
167	166	a1i	$⊢ (φ \land n \in ℕ) \to (1 \dots n) \in V$
168	101 104 29	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to M (E \cap A) \in [0, +∞]$
169		inss2	$⊢ E \cap A \subseteq A$
170		sseq2	$⊢ A = \emptyset \to (E \cap A \subseteq A \leftrightarrow E \cap A \subseteq \emptyset)$
171	169 170	mpbii	$⊢ A = \emptyset \to E \cap A \subseteq \emptyset$
172		ss0	$⊢ E \cap A \subseteq \emptyset \to E \cap A = \emptyset$
173	171 172	syl	$⊢ A = \emptyset \to E \cap A = \emptyset$
174	173	adantl	$⊢ (((φ \land n \in ℕ) \land k \in (1 \dots n)) \land A = \emptyset) \to E \cap A = \emptyset$
175	174	fveq2d	$⊢ (((φ \land n \in ℕ) \land k \in (1 \dots n)) \land A = \emptyset) \to M (E \cap A) = M (\emptyset)$
176	110	ad2antrr	$⊢ (((φ \land n \in ℕ) \land k \in (1 \dots n)) \land A = \emptyset) \to M (\emptyset) = 0$
177	175 176	eqtrd	$⊢ (((φ \land n \in ℕ) \land k \in (1 \dots n)) \land A = \emptyset) \to M (E \cap A) = 0$
178	6	adantr	$⊢ (φ \land n \in ℕ) \to \underset{k \in ℕ}{Disj} A$
179		disjss1	$⊢ (1 \dots n) \subseteq ℕ \to (\underset{k \in ℕ}{Disj} A \to {Disj}_{k = 1}^{n} A)$
180	103 178 179	sylc	$⊢ (φ \land n \in ℕ) \to {Disj}_{k = 1}^{n} A$
181	165 167 168 105 177 180	esumrnmpt2	$⊢ (φ \land n \in ℕ) \to \underset{y \in ran (k \in (1 \dots n) ⟼ A)}{\sum^{}} M (E \cap y) = {\sum^{}}_{k = 1}^{n} M (E \cap A)$
182	153 163 181	3eqtrd	$⊢ (φ \land n \in ℕ) \to M (E \cap ⋃_{k = 1}^{n} A) = {\sum^{*}}_{k = 1}^{n} M (E \cap A)$
183	150 151 182	3eqtr3rd	$⊢ (φ \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} M (E \cap A) = M (E) +_{𝑒} (- M (E ∖ ⋃_{k = 1}^{n} A))$
184	24	adantr	$⊢ (φ \land n \in ℕ) \to M (E ∖ ⋃_{k \in ℕ} A) \in [0, +∞]$
185	12 184	sselid	$⊢ (φ \land n \in ℕ) \to M (E ∖ ⋃_{k \in ℕ} A) \in ℝ^{*}$
186	185	xnegcld	$⊢ (φ \land n \in ℕ) \to - M (E ∖ ⋃_{k \in ℕ} A) \in ℝ^{*}$
187	22	adantr	$⊢ (φ \land n \in ℕ) \to M (E) \in ℝ^{*}$
188		iunss1	$⊢ (1 \dots n) \subseteq ℕ \to ⋃_{k = 1}^{n} A \subseteq ⋃_{k \in ℕ} A$
189	102 188	mp1i	$⊢ (φ \land n \in ℕ) \to ⋃_{k = 1}^{n} A \subseteq ⋃_{k \in ℕ} A$
190	189	sscond	$⊢ (φ \land n \in ℕ) \to E ∖ ⋃_{k \in ℕ} A \subseteq E ∖ ⋃_{k = 1}^{n} A$
191	5	3adant1r	$⊢ ((φ \land n \in ℕ) \land x \subseteq y \land y \in 𝒫 O) \to M (x) \leq M (y)$
192	109 79 190 86 191	carsgmon	$⊢ (φ \land n \in ℕ) \to M (E ∖ ⋃_{k \in ℕ} A) \leq M (E ∖ ⋃_{k = 1}^{n} A)$
193		xleneg	$⊢ (M (E ∖ ⋃_{k \in ℕ} A) \in ℝ^{} \land M (E ∖ ⋃_{k = 1}^{n} A) \in ℝ^{}) \to (M (E ∖ ⋃_{k \in ℕ} A) \leq M (E ∖ ⋃_{k = 1}^{n} A) \leftrightarrow - M (E ∖ ⋃_{k = 1}^{n} A) \leq - M (E ∖ ⋃_{k \in ℕ} A))$
194	193	biimpa	$⊢ ((M (E ∖ ⋃_{k \in ℕ} A) \in ℝ^{} \land M (E ∖ ⋃_{k = 1}^{n} A) \in ℝ^{}) \land M (E ∖ ⋃_{k \in ℕ} A) \leq M (E ∖ ⋃_{k = 1}^{n} A)) \to - M (E ∖ ⋃_{k = 1}^{n} A) \leq - M (E ∖ ⋃_{k \in ℕ} A)$
195	185 88 192 194	syl21anc	$⊢ (φ \land n \in ℕ) \to - M (E ∖ ⋃_{k = 1}^{n} A) \leq - M (E ∖ ⋃_{k \in ℕ} A)$
196		xleadd2a	$⊢ ((- M (E ∖ ⋃_{k = 1}^{n} A) \in ℝ^{} \land - M (E ∖ ⋃_{k \in ℕ} A) \in ℝ^{} \land M (E) \in ℝ^{*}) \land - M (E ∖ ⋃_{k = 1}^{n} A) \leq - M (E ∖ ⋃_{k \in ℕ} A)) \to M (E) +_{𝑒} (- M (E ∖ ⋃_{k = 1}^{n} A)) \leq M (E) +_{𝑒} (- M (E ∖ ⋃_{k \in ℕ} A))$
197	91 186 187 195 196	syl31anc	$⊢ (φ \land n \in ℕ) \to M (E) +_{𝑒} (- M (E ∖ ⋃_{k = 1}^{n} A)) \leq M (E) +_{𝑒} (- M (E ∖ ⋃_{k \in ℕ} A))$
198	183 197	eqbrtrd	$⊢ (φ \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} M (E \cap A) \leq M (E) +_{𝑒} (- M (E ∖ ⋃_{k \in ℕ} A))$
199	78 29 198	esumgect	$⊢ φ \to \underset{k \in ℕ}{\sum^{*}} M (E \cap A) \leq M (E) +_{𝑒} (- M (E ∖ ⋃_{k \in ℕ} A))$
200	19 34 27 75 199	xrletrd	$⊢ φ \to M (⋃_{k \in ℕ} (E \cap A)) \leq M (E) +_{𝑒} (- M (E ∖ ⋃_{k \in ℕ} A))$
201	11 200	eqbrtrrid	$⊢ φ \to M (E \cap ⋃_{k \in ℕ} A) \leq M (E) +_{𝑒} (- M (E ∖ ⋃_{k \in ℕ} A))$
202		xleadd1a	$⊢ ((M (E \cap ⋃_{k \in ℕ} A) \in ℝ^{} \land M (E) +_{𝑒} (- M (E ∖ ⋃_{k \in ℕ} A)) \in ℝ^{} \land M (E ∖ ⋃_{k \in ℕ} A) \in ℝ^{*}) \land M (E \cap ⋃_{k \in ℕ} A) \leq M (E) +_{𝑒} (- M (E ∖ ⋃_{k \in ℕ} A))) \to M (E \cap ⋃_{k \in ℕ} A) +_{𝑒} M (E ∖ ⋃_{k \in ℕ} A) \leq (M (E) +_{𝑒} (- M (E ∖ ⋃_{k \in ℕ} A))) +_{𝑒} M (E ∖ ⋃_{k \in ℕ} A)$
203	20 27 25 201 202	syl31anc	$⊢ φ \to M (E \cap ⋃_{k \in ℕ} A) +_{𝑒} M (E ∖ ⋃_{k \in ℕ} A) \leq (M (E) +_{𝑒} (- M (E ∖ ⋃_{k \in ℕ} A))) +_{𝑒} M (E ∖ ⋃_{k \in ℕ} A)$
204		xrge0npcan	$⊢ (M (E) \in [0, +∞] \land M (E ∖ ⋃_{k \in ℕ} A) \in [0, +∞] \land M (E ∖ ⋃_{k \in ℕ} A) \leq M (E)) \to (M (E) +_{𝑒} (- M (E ∖ ⋃_{k \in ℕ} A))) +_{𝑒} M (E ∖ ⋃_{k \in ℕ} A) = M (E)$
205	21 24 77 204	syl3anc	$⊢ φ \to (M (E) +_{𝑒} (- M (E ∖ ⋃_{k \in ℕ} A))) +_{𝑒} M (E ∖ ⋃_{k \in ℕ} A) = M (E)$
206	203 205	breqtrd	$⊢ φ \to M (E \cap ⋃_{k \in ℕ} A) +_{𝑒} M (E ∖ ⋃_{k \in ℕ} A) \leq M (E)$

Metamath Proof Explorer

Theorem carsgclctunlem2

Proof