carsgclctunlem3

	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)$
	carsgclctun.1	$⊢ φ \to A ≼ ω$
	carsgclctun.2	$⊢ φ \to A \subseteq toCaraSiga (M)$
	carsgclctunlem3.1	$⊢ φ \to E \in 𝒫 O$
Assertion	carsgclctunlem3	$⊢ φ \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ 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		carsgclctun.1	$⊢ φ \to A ≼ ω$
7		carsgclctun.2	$⊢ φ \to A \subseteq toCaraSiga (M)$
8		carsgclctunlem3.1	$⊢ φ \to E \in 𝒫 O$
9		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
10	8	elpwincl1	$⊢ φ \to E \cap ⋃ A \in 𝒫 O$
11	2 10	ffvelcdmd	$⊢ φ \to M (E \cap ⋃ A) \in [0, +∞]$
12	9 11	sselid	$⊢ φ \to M (E \cap ⋃ A) \in ℝ^{*}$
13	8	elpwdifcl	$⊢ φ \to E ∖ ⋃ A \in 𝒫 O$
14	2 13	ffvelcdmd	$⊢ φ \to M (E ∖ ⋃ A) \in [0, +∞]$
15	9 14	sselid	$⊢ φ \to M (E ∖ ⋃ A) \in ℝ^{*}$
16	12 15	xaddcld	$⊢ φ \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \in ℝ^{*}$
17	16	adantr	$⊢ (φ \land M (E) = +∞) \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \in ℝ^{*}$
18		pnfge	$⊢ M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \in ℝ^{*} \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \leq +∞$
19	17 18	syl	$⊢ (φ \land M (E) = +∞) \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \leq +∞$
20		simpr	$⊢ (φ \land M (E) = +∞) \to M (E) = +∞$
21	19 20	breqtrrd	$⊢ (φ \land M (E) = +∞) \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \leq M (E)$
22		unieq	$⊢ A = \emptyset \to ⋃ A = ⋃ \emptyset$
23		uni0	$⊢ ⋃ \emptyset = \emptyset$
24	22 23	eqtrdi	$⊢ A = \emptyset \to ⋃ A = \emptyset$
25	24	ineq2d	$⊢ A = \emptyset \to E \cap ⋃ A = E \cap \emptyset$
26		in0	$⊢ E \cap \emptyset = \emptyset$
27	25 26	eqtrdi	$⊢ A = \emptyset \to E \cap ⋃ A = \emptyset$
28	27	fveq2d	$⊢ A = \emptyset \to M (E \cap ⋃ A) = M (\emptyset)$
29	24	difeq2d	$⊢ A = \emptyset \to E ∖ ⋃ A = E ∖ \emptyset$
30		dif0	$⊢ E ∖ \emptyset = E$
31	29 30	eqtrdi	$⊢ A = \emptyset \to E ∖ ⋃ A = E$
32	31	fveq2d	$⊢ A = \emptyset \to M (E ∖ ⋃ A) = M (E)$
33	28 32	oveq12d	$⊢ A = \emptyset \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) = M (\emptyset) +_{𝑒} M (E)$
34	33	adantl	$⊢ (φ \land A = \emptyset) \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) = M (\emptyset) +_{𝑒} M (E)$
35	3	adantr	$⊢ (φ \land A = \emptyset) \to M (\emptyset) = 0$
36	35	oveq1d	$⊢ (φ \land A = \emptyset) \to M (\emptyset) +_{𝑒} M (E) = 0 +_{𝑒} M (E)$
37	2 8	ffvelcdmd	$⊢ φ \to M (E) \in [0, +∞]$
38	9 37	sselid	$⊢ φ \to M (E) \in ℝ^{*}$
39	38	adantr	$⊢ (φ \land A = \emptyset) \to M (E) \in ℝ^{*}$
40		xaddlid	$⊢ M (E) \in ℝ^{*} \to 0 +_{𝑒} M (E) = M (E)$
41	39 40	syl	$⊢ (φ \land A = \emptyset) \to 0 +_{𝑒} M (E) = M (E)$
42	34 36 41	3eqtrd	$⊢ (φ \land A = \emptyset) \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) = M (E)$
43	42 39	eqeltrd	$⊢ (φ \land A = \emptyset) \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \in ℝ^{*}$
44		xeqlelt	$⊢ (M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \in ℝ^{} \land M (E) \in ℝ^{}) \to (M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) = M (E) \leftrightarrow (M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \leq M (E) \land \neg M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) < M (E)))$
45	43 39 44	syl2anc	$⊢ (φ \land A = \emptyset) \to (M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) = M (E) \leftrightarrow (M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \leq M (E) \land \neg M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) < M (E)))$
46	42 45	mpbid	$⊢ (φ \land A = \emptyset) \to (M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \leq M (E) \land \neg M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) < M (E))$
47	46	simpld	$⊢ (φ \land A = \emptyset) \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \leq M (E)$
48	47	adantlr	$⊢ ((φ \land M (E) \neq +∞) \land A = \emptyset) \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \leq M (E)$
49		fvex	$⊢ toCaraSiga (M) \in V$
50	49	ssex	$⊢ A \subseteq toCaraSiga (M) \to A \in V$
51		0sdomg	$⊢ A \in V \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
52	7 50 51	3syl	$⊢ φ \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
53	52	biimpar	$⊢ (φ \land A \neq \emptyset) \to \emptyset ≺ A$
54	53	adantlr	$⊢ ((φ \land M (E) \neq +∞) \land A \neq \emptyset) \to \emptyset ≺ A$
55		nnenom	$⊢ ℕ \approx ω$
56	55	ensymi	$⊢ ω \approx ℕ$
57		domentr	$⊢ (A ≼ ω \land ω \approx ℕ) \to A ≼ ℕ$
58	6 56 57	sylancl	$⊢ φ \to A ≼ ℕ$
59	58	ad2antrr	$⊢ ((φ \land M (E) \neq +∞) \land A \neq \emptyset) \to A ≼ ℕ$
60		fodomr	$⊢ (\emptyset ≺ A \land A ≼ ℕ) \to \exists f f : ℕ \underset{onto}{⟶} A$
61	54 59 60	syl2anc	$⊢ ((φ \land M (E) \neq +∞) \land A \neq \emptyset) \to \exists f f : ℕ \underset{onto}{⟶} A$
62		fveq2	$⊢ n = k \to f (n) = f (k)$
63	62	iundisj	$⊢ ⋃_{n \in ℕ} f (n) = ⋃_{n \in ℕ} (f (n) ∖ ⋃_{k \in (1 ..^n)} f (k))$
64		fofn	$⊢ f : ℕ \underset{onto}{⟶} A \to f Fn ℕ$
65		fniunfv	$⊢ f Fn ℕ \to ⋃_{n \in ℕ} f (n) = ⋃ ran f$
66	64 65	syl	$⊢ f : ℕ \underset{onto}{⟶} A \to ⋃_{n \in ℕ} f (n) = ⋃ ran f$
67		forn	$⊢ f : ℕ \underset{onto}{⟶} A \to ran f = A$
68	67	unieqd	$⊢ f : ℕ \underset{onto}{⟶} A \to ⋃ ran f = ⋃ A$
69	66 68	eqtrd	$⊢ f : ℕ \underset{onto}{⟶} A \to ⋃_{n \in ℕ} f (n) = ⋃ A$
70	69	adantl	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to ⋃_{n \in ℕ} f (n) = ⋃ A$
71	63 70	eqtr3id	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to ⋃_{n \in ℕ} (f (n) ∖ ⋃_{k \in (1 ..^n)} f (k)) = ⋃ A$
72	71	ineq2d	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to E \cap ⋃_{n \in ℕ} (f (n) ∖ ⋃_{k \in (1 ..^n)} f (k)) = E \cap ⋃ A$
73	72	fveq2d	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to M (E \cap ⋃_{n \in ℕ} (f (n) ∖ ⋃_{k \in (1 ..^n)} f (k))) = M (E \cap ⋃ A)$
74	71	difeq2d	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to E ∖ ⋃_{n \in ℕ} (f (n) ∖ ⋃_{k \in (1 ..^n)} f (k)) = E ∖ ⋃ A$
75	74	fveq2d	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to M (E ∖ ⋃_{n \in ℕ} (f (n) ∖ ⋃_{k \in (1 ..^n)} f (k))) = M (E ∖ ⋃ A)$
76	73 75	oveq12d	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to M (E \cap ⋃_{n \in ℕ} (f (n) ∖ ⋃_{k \in (1 ..^n)} f (k))) +_{𝑒} M (E ∖ ⋃_{n \in ℕ} (f (n) ∖ ⋃_{k \in (1 ..^n)} f (k))) = M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A)$
77	1	ad3antrrr	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to O \in V$
78	2	ad3antrrr	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to M : 𝒫 O ⟶ [0, +∞]$
79	3	ad3antrrr	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to M (\emptyset) = 0$
80	4	3adant1r	$⊢ ((φ \land M (E) \neq +∞) \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
81	80	3adant1r	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
82	81	3adant1r	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
83	5	3adant1r	$⊢ ((φ \land M (E) \neq +∞) \land x \subseteq y \land y \in 𝒫 O) \to M (x) \leq M (y)$
84	83	3adant1r	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land x \subseteq y \land y \in 𝒫 O) \to M (x) \leq M (y)$
85	84	3adant1r	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land x \subseteq y \land y \in 𝒫 O) \to M (x) \leq M (y)$
86	62	iundisj2	$⊢ \underset{n \in ℕ}{Disj} (f (n) ∖ ⋃_{k \in (1 ..^n)} f (k))$
87	86	a1i	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to \underset{n \in ℕ}{Disj} (f (n) ∖ ⋃_{k \in (1 ..^n)} f (k))$
88	77	adantr	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to O \in V$
89	78	adantr	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to M : 𝒫 O ⟶ [0, +∞]$
90	7	ad4antr	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to A \subseteq toCaraSiga (M)$
91		fof	$⊢ f : ℕ \underset{onto}{⟶} A \to f : ℕ ⟶ A$
92	91	ad2antlr	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to f : ℕ ⟶ A$
93		simpr	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to n \in ℕ$
94	92 93	ffvelcdmd	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to f (n) \in A$
95	90 94	sseldd	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to f (n) \in toCaraSiga (M)$
96	79	adantr	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to M (\emptyset) = 0$
97	82	3adant1r	$⊢ (((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
98	88 89 96 97	carsgsigalem	$⊢ (((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \land e \in 𝒫 O \land g \in 𝒫 O) \to M (e \cup g) \leq M (e) +_{𝑒} M (g)$
99	91	ad3antlr	$⊢ (((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \land k \in (1 ..^n)) \to f : ℕ ⟶ A$
100		fzossnn	$⊢ (1 ..^n) \subseteq ℕ$
101	100	a1i	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to (1 ..^n) \subseteq ℕ$
102	101	sselda	$⊢ (((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \land k \in (1 ..^n)) \to k \in ℕ$
103	99 102	ffvelcdmd	$⊢ (((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \land k \in (1 ..^n)) \to f (k) \in A$
104	103	ralrimiva	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to \forall k \in (1 ..^n) f (k) \in A$
105		dfiun2g	$⊢ \forall k \in (1 ..^n) f (k) \in A \to ⋃_{k \in (1 ..^n)} f (k) = ⋃ \{z \| \exists k \in (1 ..^n) z = f (k)\}$
106	104 105	syl	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to ⋃_{k \in (1 ..^n)} f (k) = ⋃ \{z \| \exists k \in (1 ..^n) z = f (k)\}$
107		eqid	$⊢ (k \in (1 ..^n) ⟼ f (k)) = (k \in (1 ..^n) ⟼ f (k))$
108	107	rnmpt	$⊢ ran (k \in (1 ..^n) ⟼ f (k)) = \{z \| \exists k \in (1 ..^n) z = f (k)\}$
109		fzofi	$⊢ (1 ..^n) \in Fin$
110		mptfi	$⊢ (1 ..^n) \in Fin \to (k \in (1 ..^n) ⟼ f (k)) \in Fin$
111		rnfi	$⊢ (k \in (1 ..^n) ⟼ f (k)) \in Fin \to ran (k \in (1 ..^n) ⟼ f (k)) \in Fin$
112	109 110 111	mp2b	$⊢ ran (k \in (1 ..^n) ⟼ f (k)) \in Fin$
113	108 112	eqeltrri	$⊢ \{z \| \exists k \in (1 ..^n) z = f (k)\} \in Fin$
114	113	a1i	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to \{z \| \exists k \in (1 ..^n) z = f (k)\} \in Fin$
115	90	adantr	$⊢ (((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \land k \in (1 ..^n)) \to A \subseteq toCaraSiga (M)$
116	115 103	sseldd	$⊢ (((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \land k \in (1 ..^n)) \to f (k) \in toCaraSiga (M)$
117	116	ralrimiva	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to \forall k \in (1 ..^n) f (k) \in toCaraSiga (M)$
118	107	rnmptss	$⊢ \forall k \in (1 ..^n) f (k) \in toCaraSiga (M) \to ran (k \in (1 ..^n) ⟼ f (k)) \subseteq toCaraSiga (M)$
119	117 118	syl	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to ran (k \in (1 ..^n) ⟼ f (k)) \subseteq toCaraSiga (M)$
120	108 119	eqsstrrid	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to \{z \| \exists k \in (1 ..^n) z = f (k)\} \subseteq toCaraSiga (M)$
121	88 89 96 97 114 120	fiunelcarsg	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to ⋃ \{z \| \exists k \in (1 ..^n) z = f (k)\} \in toCaraSiga (M)$
122	106 121	eqeltrd	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to ⋃_{k \in (1 ..^n)} f (k) \in toCaraSiga (M)$
123	88 89 95 98 122	difelcarsg2	$⊢ ((((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \land n \in ℕ) \to f (n) ∖ ⋃_{k \in (1 ..^n)} f (k) \in toCaraSiga (M)$
124	8	ad3antrrr	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to E \in 𝒫 O$
125		simpllr	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to M (E) \neq +∞$
126	77 78 79 82 85 87 123 124 125	carsgclctunlem2	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to M (E \cap ⋃_{n \in ℕ} (f (n) ∖ ⋃_{k \in (1 ..^n)} f (k))) +_{𝑒} M (E ∖ ⋃_{n \in ℕ} (f (n) ∖ ⋃_{k \in (1 ..^n)} f (k))) \leq M (E)$
127	76 126	eqbrtrrd	$⊢ (((φ \land M (E) \neq +∞) \land A \neq \emptyset) \land f : ℕ \underset{onto}{⟶} A) \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \leq M (E)$
128	61 127	exlimddv	$⊢ ((φ \land M (E) \neq +∞) \land A \neq \emptyset) \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \leq M (E)$
129	48 128	pm2.61dane	$⊢ (φ \land M (E) \neq +∞) \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \leq M (E)$
130	21 129	pm2.61dane	$⊢ φ \to M (E \cap ⋃ A) +_{𝑒} M (E ∖ ⋃ A) \leq M (E)$

Metamath Proof Explorer

Theorem carsgclctunlem3

Proof