carsggect

Description: The outer measure is countably superadditive on Caratheodory measurable sets. (Contributed by Thierry Arnoux, 31-May-2020)

	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)$
	carsggect.0	$⊢ φ \to \neg \emptyset \in A$
	carsggect.1	$⊢ φ \to A ≼ ω$
	carsggect.2	$⊢ φ \to A \subseteq toCaraSiga (M)$
	carsggect.3	$⊢ φ \to \underset{y \in A}{Disj} y$
	carsggect.4	$⊢ (φ \land x \subseteq y \land y \in 𝒫 O) \to M (x) \leq M (y)$
Assertion	carsggect	$⊢ φ \to \underset{z \in A}{\sum^{*}} M (z) \leq M (⋃ A)$

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		carsggect.0	$⊢ φ \to \neg \emptyset \in A$
6		carsggect.1	$⊢ φ \to A ≼ ω$
7		carsggect.2	$⊢ φ \to A \subseteq toCaraSiga (M)$
8		carsggect.3	$⊢ φ \to \underset{y \in A}{Disj} y$
9		carsggect.4	$⊢ (φ \land x \subseteq y \land y \in 𝒫 O) \to M (x) \leq M (y)$
10		0ex	$⊢ \emptyset \in V$
11	10	a1i	$⊢ φ \to \emptyset \in V$
12		padct	$⊢ (A ≼ ω \land \emptyset \in V \land \neg \emptyset \in A) \to \exists f (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))$
13	6 11 5 12	syl3anc	$⊢ φ \to \exists f (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))$
14		nfv	$⊢ Ⅎ z (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A})))$
15		simpr1	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to f : ℕ ⟶ A \cup \{\emptyset\}$
16	15	feqmptd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to f = (k \in ℕ ⟼ f (k))$
17	16	rneqd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ran f = ran (k \in ℕ ⟼ f (k))$
18	14 17	esumeq1d	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{z \in ran f}{\sum^{}} M (z) = \underset{z \in ran (k \in ℕ ⟼ f (k))}{\sum^{}} M (z)$
19		fvex	$⊢ toCaraSiga (M) \in V$
20	19	a1i	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to toCaraSiga (M) \in V$
21	7	adantr	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to A \subseteq toCaraSiga (M)$
22	1	adantr	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to O \in V$
23	2	adantr	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to M : 𝒫 O ⟶ [0, +∞]$
24	3	adantr	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to M (\emptyset) = 0$
25	22 23 24	0elcarsg	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \emptyset \in toCaraSiga (M)$
26	25	snssd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \{\emptyset\} \subseteq toCaraSiga (M)$
27	21 26	unssd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to A \cup \{\emptyset\} \subseteq toCaraSiga (M)$
28	20 27	ssexd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to A \cup \{\emptyset\} \in V$
29	23	adantr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land z \in (A \cup \{\emptyset\})) \to M : 𝒫 O ⟶ [0, +∞]$
30	1 2	carsgcl	$⊢ φ \to toCaraSiga (M) \subseteq 𝒫 O$
31	7 30	sstrd	$⊢ φ \to A \subseteq 𝒫 O$
32	31	adantr	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to A \subseteq 𝒫 O$
33		0elpw	$⊢ \emptyset \in 𝒫 O$
34	33	a1i	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \emptyset \in 𝒫 O$
35	34	snssd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \{\emptyset\} \subseteq 𝒫 O$
36	32 35	unssd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to A \cup \{\emptyset\} \subseteq 𝒫 O$
37	36	sselda	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land z \in (A \cup \{\emptyset\})) \to z \in 𝒫 O$
38	29 37	ffvelrnd	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land z \in (A \cup \{\emptyset\})) \to M (z) \in [0, +∞]$
39	15	frnd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ran f \subseteq A \cup \{\emptyset\}$
40	14 28 38 39	esummono	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{z \in ran f}{\sum^{}} M (z) \leq \underset{z \in A \cup \{\emptyset\}}{\sum^{}} M (z)$
41		ctex	$⊢ A ≼ ω \to A \in V$
42	6 41	syl	$⊢ φ \to A \in V$
43	42	adantr	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to A \in V$
44	20 26	ssexd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \{\emptyset\} \in V$
45	23	adantr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land z \in A) \to M : 𝒫 O ⟶ [0, +∞]$
46	32	sselda	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land z \in A) \to z \in 𝒫 O$
47	45 46	ffvelrnd	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land z \in A) \to M (z) \in [0, +∞]$
48		elsni	$⊢ z \in \{\emptyset\} \to z = \emptyset$
49	48	adantl	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land z \in \{\emptyset\}) \to z = \emptyset$
50	49	fveq2d	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land z \in \{\emptyset\}) \to M (z) = M (\emptyset)$
51	24	adantr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land z \in \{\emptyset\}) \to M (\emptyset) = 0$
52	50 51	eqtrd	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land z \in \{\emptyset\}) \to M (z) = 0$
53	43 44 47 52	esumpad	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{z \in A \cup \{\emptyset\}}{\sum^{}} M (z) = \underset{z \in A}{\sum^{}} M (z)$
54	40 53	breqtrd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{z \in ran f}{\sum^{}} M (z) \leq \underset{z \in A}{\sum^{}} M (z)$
55	39 27	sstrd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ran f \subseteq toCaraSiga (M)$
56		ssexg	$⊢ (ran f \subseteq toCaraSiga (M) \land toCaraSiga (M) \in V) \to ran f \in V$
57	55 19 56	sylancl	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ran f \in V$
58	23	adantr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land z \in ran f) \to M : 𝒫 O ⟶ [0, +∞]$
59	39 36	sstrd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ran f \subseteq 𝒫 O$
60	59	sselda	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land z \in ran f) \to z \in 𝒫 O$
61	58 60	ffvelrnd	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land z \in ran f) \to M (z) \in [0, +∞]$
62		simpr2	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to A \subseteq ran f$
63	14 57 61 62	esummono	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{z \in A}{\sum^{}} M (z) \leq \underset{z \in ran f}{\sum^{}} M (z)$
64	54 63	jca	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to (\underset{z \in ran f}{\sum^{}} M (z) \leq \underset{z \in A}{\sum^{}} M (z) \land \underset{z \in A}{\sum^{}} M (z) \leq \underset{z \in ran f}{\sum^{}} M (z))$
65		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
66	61	ralrimiva	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \forall z \in ran f M (z) \in [0, +∞]$
67		nfcv	$⊢ \underline{Ⅎ} z ran f$
68	67	esumcl	$⊢ (ran f \in V \land \forall z \in ran f M (z) \in [0, +∞]) \to \underset{z \in ran f}{\sum^{*}} M (z) \in [0, +∞]$
69	57 66 68	syl2anc	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{z \in ran f}{\sum^{*}} M (z) \in [0, +∞]$
70	65 69	sseldi	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{z \in ran f}{\sum^{}} M (z) \in ℝ^{}$
71	47	ralrimiva	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \forall z \in A M (z) \in [0, +∞]$
72		nfcv	$⊢ \underline{Ⅎ} z A$
73	72	esumcl	$⊢ (A \in V \land \forall z \in A M (z) \in [0, +∞]) \to \underset{z \in A}{\sum^{*}} M (z) \in [0, +∞]$
74	43 71 73	syl2anc	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{z \in A}{\sum^{*}} M (z) \in [0, +∞]$
75	65 74	sseldi	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{z \in A}{\sum^{}} M (z) \in ℝ^{}$
76		xrletri3	$⊢ (\underset{z \in ran f}{\sum^{}} M (z) \in ℝ^{} \land \underset{z \in A}{\sum^{}} M (z) \in ℝ^{}) \to (\underset{z \in ran f}{\sum^{}} M (z) = \underset{z \in A}{\sum^{}} M (z) \leftrightarrow (\underset{z \in ran f}{\sum^{}} M (z) \leq \underset{z \in A}{\sum^{}} M (z) \land \underset{z \in A}{\sum^{}} M (z) \leq \underset{z \in ran f}{\sum^{}} M (z)))$
77	70 75 76	syl2anc	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to (\underset{z \in ran f}{\sum^{}} M (z) = \underset{z \in A}{\sum^{}} M (z) \leftrightarrow (\underset{z \in ran f}{\sum^{}} M (z) \leq \underset{z \in A}{\sum^{}} M (z) \land \underset{z \in A}{\sum^{}} M (z) \leq \underset{z \in ran f}{\sum^{}} M (z)))$
78	64 77	mpbird	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{z \in ran f}{\sum^{}} M (z) = \underset{z \in A}{\sum^{}} M (z)$
79		fveq2	$⊢ z = f (k) \to M (z) = M (f (k))$
80		nnex	$⊢ ℕ \in V$
81	80	a1i	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ℕ \in V$
82	23	adantr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in ℕ) \to M : 𝒫 O ⟶ [0, +∞]$
83	36	adantr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in ℕ) \to A \cup \{\emptyset\} \subseteq 𝒫 O$
84	15	adantr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in ℕ) \to f : ℕ ⟶ A \cup \{\emptyset\}$
85		simpr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in ℕ) \to k \in ℕ$
86	84 85	ffvelrnd	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in ℕ) \to f (k) \in (A \cup \{\emptyset\})$
87	83 86	sseldd	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in ℕ) \to f (k) \in 𝒫 O$
88	82 87	ffvelrnd	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in ℕ) \to M (f (k)) \in [0, +∞]$
89		simpr	$⊢ (((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in ℕ) \land f (k) = \emptyset) \to f (k) = \emptyset$
90	89	fveq2d	$⊢ (((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in ℕ) \land f (k) = \emptyset) \to M (f (k)) = M (\emptyset)$
91	24	ad2antrr	$⊢ (((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in ℕ) \land f (k) = \emptyset) \to M (\emptyset) = 0$
92	90 91	eqtrd	$⊢ (((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in ℕ) \land f (k) = \emptyset) \to M (f (k)) = 0$
93		cnvimass	$⊢ f^{-1} [A] \subseteq dom f$
94	93 15	fssdm	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to f^{-1} [A] \subseteq ℕ$
95		ffun	$⊢ f : ℕ ⟶ A \cup \{\emptyset\} \to Fun f$
96	15 95	syl	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to Fun f$
97	96	adantr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in (ℕ ∖ f^{-1} [A])) \to Fun f$
98		difpreima	$⊢ Fun f \to f^{-1} [(A \cup \{\emptyset\}) ∖ A] = f^{-1} [A \cup \{\emptyset\}] ∖ f^{-1} [A]$
99	15 95 98	3syl	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to f^{-1} [(A \cup \{\emptyset\}) ∖ A] = f^{-1} [A \cup \{\emptyset\}] ∖ f^{-1} [A]$
100		fimacnv	$⊢ f : ℕ ⟶ A \cup \{\emptyset\} \to f^{-1} [A \cup \{\emptyset\}] = ℕ$
101	15 100	syl	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to f^{-1} [A \cup \{\emptyset\}] = ℕ$
102	101	difeq1d	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to f^{-1} [A \cup \{\emptyset\}] ∖ f^{-1} [A] = ℕ ∖ f^{-1} [A]$
103	99 102	eqtrd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to f^{-1} [(A \cup \{\emptyset\}) ∖ A] = ℕ ∖ f^{-1} [A]$
104		uncom	$⊢ \{\emptyset\} \cup A = A \cup \{\emptyset\}$
105	104	difeq1i	$⊢ (\{\emptyset\} \cup A) ∖ A = (A \cup \{\emptyset\}) ∖ A$
106		difun2	$⊢ (\{\emptyset\} \cup A) ∖ A = \{\emptyset\} ∖ A$
107	105 106	eqtr3i	$⊢ (A \cup \{\emptyset\}) ∖ A = \{\emptyset\} ∖ A$
108		difss	$⊢ \{\emptyset\} ∖ A \subseteq \{\emptyset\}$
109	107 108	eqsstri	$⊢ (A \cup \{\emptyset\}) ∖ A \subseteq \{\emptyset\}$
110	109	a1i	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to (A \cup \{\emptyset\}) ∖ A \subseteq \{\emptyset\}$
111		sspreima	$⊢ (Fun f \land (A \cup \{\emptyset\}) ∖ A \subseteq \{\emptyset\}) \to f^{-1} [(A \cup \{\emptyset\}) ∖ A] \subseteq f^{-1} [\{\emptyset\}]$
112	96 110 111	syl2anc	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to f^{-1} [(A \cup \{\emptyset\}) ∖ A] \subseteq f^{-1} [\{\emptyset\}]$
113	103 112	eqsstrrd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ℕ ∖ f^{-1} [A] \subseteq f^{-1} [\{\emptyset\}]$
114	113	sselda	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in (ℕ ∖ f^{-1} [A])) \to k \in f^{-1} [\{\emptyset\}]$
115		fvimacnvi	$⊢ (Fun f \land k \in f^{-1} [\{\emptyset\}]) \to f (k) \in \{\emptyset\}$
116	97 114 115	syl2anc	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in (ℕ ∖ f^{-1} [A])) \to f (k) \in \{\emptyset\}$
117		elsni	$⊢ f (k) \in \{\emptyset\} \to f (k) = \emptyset$
118	116 117	syl	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in (ℕ ∖ f^{-1} [A])) \to f (k) = \emptyset$
119	118	ralrimiva	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \forall k \in (ℕ ∖ f^{-1} [A]) f (k) = \emptyset$
120	8	adantr	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{y \in A}{Disj} y$
121		simpr3	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to Fun ({f^{-1} ↾}_{A})$
122		fresf1o	$⊢ (Fun f \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A})) \to ({f ↾}_{f^{-1} [A]}) : f^{-1} [A] \underset{1-1 onto}{⟶} A$
123	96 62 121 122	syl3anc	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ({f ↾}_{f^{-1} [A]}) : f^{-1} [A] \underset{1-1 onto}{⟶} A$
124		simpr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land y = ({f ↾}_{f^{-1} [A]}) (k)) \to y = ({f ↾}_{f^{-1} [A]}) (k)$
125	123 124	disjrdx	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to (\underset{k \in f^{-1} [A]}{Disj} ({f ↾}_{f^{-1} [A]}) (k) \leftrightarrow \underset{y \in A}{Disj} y)$
126		fvres	$⊢ k \in f^{-1} [A] \to ({f ↾}_{f^{-1} [A]}) (k) = f (k)$
127	126	adantl	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land k \in f^{-1} [A]) \to ({f ↾}_{f^{-1} [A]}) (k) = f (k)$
128	127	disjeq2dv	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to (\underset{k \in f^{-1} [A]}{Disj} ({f ↾}_{f^{-1} [A]}) (k) \leftrightarrow \underset{k \in f^{-1} [A]}{Disj} f (k))$
129	125 128	bitr3d	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to (\underset{y \in A}{Disj} y \leftrightarrow \underset{k \in f^{-1} [A]}{Disj} f (k))$
130	120 129	mpbid	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{k \in f^{-1} [A]}{Disj} f (k)$
131		disjss3	$⊢ (f^{-1} [A] \subseteq ℕ \land \forall k \in (ℕ ∖ f^{-1} [A]) f (k) = \emptyset) \to (\underset{k \in f^{-1} [A]}{Disj} f (k) \leftrightarrow \underset{k \in ℕ}{Disj} f (k))$
132	131	biimpa	$⊢ ((f^{-1} [A] \subseteq ℕ \land \forall k \in (ℕ ∖ f^{-1} [A]) f (k) = \emptyset) \land \underset{k \in f^{-1} [A]}{Disj} f (k)) \to \underset{k \in ℕ}{Disj} f (k)$
133	94 119 130 132	syl21anc	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{k \in ℕ}{Disj} f (k)$
134	79 81 88 87 92 133	esumrnmpt2	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{z \in ran (k \in ℕ ⟼ f (k))}{\sum^{}} M (z) = \underset{k \in ℕ}{\sum^{}} M (f (k))$
135	18 78 134	3eqtr3rd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{k \in ℕ}{\sum^{}} M (f (k)) = \underset{z \in A}{\sum^{}} M (z)$
136		uniiun	$⊢ ⋃ A = ⋃_{x \in A} x$
137	31	sselda	$⊢ (φ \land x \in A) \to x \in 𝒫 O$
138	42 137	elpwiuncl	$⊢ φ \to ⋃_{x \in A} x \in 𝒫 O$
139	136 138	eqeltrid	$⊢ φ \to ⋃ A \in 𝒫 O$
140	139	adantr	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ⋃ A \in 𝒫 O$
141	23 140	ffvelrnd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to M (⋃ A) \in [0, +∞]$
142	4	3adant1r	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
143		fveq2	$⊢ y = z \to M (y) = M (z)$
144		nfcv	$⊢ \underline{Ⅎ} z x$
145		nfcv	$⊢ \underline{Ⅎ} y x$
146		nfcv	$⊢ \underline{Ⅎ} z M (y)$
147		nfcv	$⊢ \underline{Ⅎ} y M (z)$
148	143 144 145 146 147	cbvesum	$⊢ \underset{y \in x}{\sum^{}} M (y) = \underset{z \in x}{\sum^{}} M (z)$
149	142 148	breqtrdi	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{z \in x}{\sum^{*}} M (z)$
150		ffn	$⊢ f : ℕ ⟶ A \cup \{\emptyset\} \to f Fn ℕ$
151		fz1ssnn	$⊢ (1 \dots n) \subseteq ℕ$
152		fnssres	$⊢ (f Fn ℕ \land (1 \dots n) \subseteq ℕ) \to ({f ↾}_{(1 \dots n)}) Fn (1 \dots n)$
153	151 152	mpan2	$⊢ f Fn ℕ \to ({f ↾}_{(1 \dots n)}) Fn (1 \dots n)$
154	15 150 153	3syl	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ({f ↾}_{(1 \dots n)}) Fn (1 \dots n)$
155		fzfi	$⊢ (1 \dots n) \in Fin$
156		fnfi	$⊢ (({f ↾}_{(1 \dots n)}) Fn (1 \dots n) \land (1 \dots n) \in Fin) \to {f ↾}_{(1 \dots n)} \in Fin$
157	155 156	mpan2	$⊢ ({f ↾}_{(1 \dots n)}) Fn (1 \dots n) \to {f ↾}_{(1 \dots n)} \in Fin$
158		rnfi	$⊢ {f ↾}_{(1 \dots n)} \in Fin \to ran ({f ↾}_{(1 \dots n)}) \in Fin$
159	154 157 158	3syl	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ran ({f ↾}_{(1 \dots n)}) \in Fin$
160		resss	$⊢ {f ↾}_{(1 \dots n)} \subseteq f$
161		rnss	$⊢ {f ↾}_{(1 \dots n)} \subseteq f \to ran ({f ↾}_{(1 \dots n)}) \subseteq ran f$
162	160 161	ax-mp	$⊢ ran ({f ↾}_{(1 \dots n)}) \subseteq ran f$
163	162	a1i	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ran ({f ↾}_{(1 \dots n)}) \subseteq ran f$
164	163 55	sstrd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ran ({f ↾}_{(1 \dots n)}) \subseteq toCaraSiga (M)$
165	163 39	sstrd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ran ({f ↾}_{(1 \dots n)}) \subseteq A \cup \{\emptyset\}$
166		nfcv	$⊢ \underline{Ⅎ} z y$
167		nfcv	$⊢ \underline{Ⅎ} y z$
168		id	$⊢ y = z \to y = z$
169	166 167 168	cbvdisj	$⊢ \underset{y \in A}{Disj} y \leftrightarrow \underset{z \in A}{Disj} z$
170		disjun0	$⊢ \underset{z \in A}{Disj} z \to \underset{z \in A \cup \{\emptyset\}}{Disj} z$
171	169 170	sylbi	$⊢ \underset{y \in A}{Disj} y \to \underset{z \in A \cup \{\emptyset\}}{Disj} z$
172	8 171	syl	$⊢ φ \to \underset{z \in A \cup \{\emptyset\}}{Disj} z$
173	172	adantr	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{z \in A \cup \{\emptyset\}}{Disj} z$
174		disjss1	$⊢ ran ({f ↾}_{(1 \dots n)}) \subseteq A \cup \{\emptyset\} \to (\underset{z \in A \cup \{\emptyset\}}{Disj} z \to \underset{z \in ran ({f ↾}_{(1 \dots n)})}{Disj} z)$
175	165 173 174	sylc	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{z \in ran ({f ↾}_{(1 \dots n)})}{Disj} z$
176		pwidg	$⊢ O \in V \to O \in 𝒫 O$
177	22 176	syl	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to O \in 𝒫 O$
178	22 23 24 149 159 164 175 177	carsgclctunlem1	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to M (O \cap ⋃ ran ({f ↾}_{(1 \dots n)})) = \underset{z \in ran ({f ↾}_{(1 \dots n)})}{\sum^{*}} M (O \cap z)$
179	178	adantr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to M (O \cap ⋃ ran ({f ↾}_{(1 \dots n)})) = \underset{z \in ran ({f ↾}_{(1 \dots n)})}{\sum^{*}} M (O \cap z)$
180	165	unissd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ⋃ ran ({f ↾}_{(1 \dots n)}) \subseteq ⋃ (A \cup \{\emptyset\})$
181		uniun	$⊢ ⋃ (A \cup \{\emptyset\}) = ⋃ A \cup ⋃ \{\emptyset\}$
182	10	unisn	$⊢ ⋃ \{\emptyset\} = \emptyset$
183	182	uneq2i	$⊢ ⋃ A \cup ⋃ \{\emptyset\} = ⋃ A \cup \emptyset$
184		un0	$⊢ ⋃ A \cup \emptyset = ⋃ A$
185	181 183 184	3eqtri	$⊢ ⋃ (A \cup \{\emptyset\}) = ⋃ A$
186	180 185	sseqtrdi	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to ⋃ ran ({f ↾}_{(1 \dots n)}) \subseteq ⋃ A$
187	186	adantr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to ⋃ ran ({f ↾}_{(1 \dots n)}) \subseteq ⋃ A$
188		uniss	$⊢ A \subseteq 𝒫 O \to ⋃ A \subseteq ⋃ 𝒫 O$
189		unipw	$⊢ ⋃ 𝒫 O = O$
190	188 189	sseqtrdi	$⊢ A \subseteq 𝒫 O \to ⋃ A \subseteq O$
191	31 190	syl	$⊢ φ \to ⋃ A \subseteq O$
192	191	ad2antrr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to ⋃ A \subseteq O$
193	187 192	sstrd	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to ⋃ ran ({f ↾}_{(1 \dots n)}) \subseteq O$
194		sseqin2	$⊢ ⋃ ran ({f ↾}_{(1 \dots n)}) \subseteq O \leftrightarrow O \cap ⋃ ran ({f ↾}_{(1 \dots n)}) = ⋃ ran ({f ↾}_{(1 \dots n)})$
195	193 194	sylib	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to O \cap ⋃ ran ({f ↾}_{(1 \dots n)}) = ⋃ ran ({f ↾}_{(1 \dots n)})$
196	195	fveq2d	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to M (O \cap ⋃ ran ({f ↾}_{(1 \dots n)})) = M (⋃ ran ({f ↾}_{(1 \dots n)}))$
197		nfv	$⊢ Ⅎ z ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ)$
198	165	adantr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to ran ({f ↾}_{(1 \dots n)}) \subseteq A \cup \{\emptyset\}$
199	31	ad2antrr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to A \subseteq 𝒫 O$
200	33	a1i	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to \emptyset \in 𝒫 O$
201	200	snssd	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to \{\emptyset\} \subseteq 𝒫 O$
202	199 201	unssd	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to A \cup \{\emptyset\} \subseteq 𝒫 O$
203	198 202	sstrd	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to ran ({f ↾}_{(1 \dots n)}) \subseteq 𝒫 O$
204	203	sselda	$⊢ (((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \land z \in ran ({f ↾}_{(1 \dots n)})) \to z \in 𝒫 O$
205	204	elpwid	$⊢ (((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \land z \in ran ({f ↾}_{(1 \dots n)})) \to z \subseteq O$
206		sseqin2	$⊢ z \subseteq O \leftrightarrow O \cap z = z$
207	205 206	sylib	$⊢ (((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \land z \in ran ({f ↾}_{(1 \dots n)})) \to O \cap z = z$
208	207	fveq2d	$⊢ (((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \land z \in ran ({f ↾}_{(1 \dots n)})) \to M (O \cap z) = M (z)$
209	208	ralrimiva	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to \forall z \in ran ({f ↾}_{(1 \dots n)}) M (O \cap z) = M (z)$
210	197 209	esumeq2d	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to \underset{z \in ran ({f ↾}_{(1 \dots n)})}{\sum^{}} M (O \cap z) = \underset{z \in ran ({f ↾}_{(1 \dots n)})}{\sum^{}} M (z)$
211	16	reseq1d	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to {f ↾}_{(1 \dots n)} = {(k \in ℕ ⟼ f (k)) ↾}_{(1 \dots n)}$
212	211	adantr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to {f ↾}_{(1 \dots n)} = {(k \in ℕ ⟼ f (k)) ↾}_{(1 \dots n)}$
213		resmpt	$⊢ (1 \dots n) \subseteq ℕ \to {(k \in ℕ ⟼ f (k)) ↾}_{(1 \dots n)} = (k \in (1 \dots n) ⟼ f (k))$
214	151 213	ax-mp	$⊢ {(k \in ℕ ⟼ f (k)) ↾}_{(1 \dots n)} = (k \in (1 \dots n) ⟼ f (k))$
215	212 214	eqtrdi	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to {f ↾}_{(1 \dots n)} = (k \in (1 \dots n) ⟼ f (k))$
216	215	eqcomd	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to (k \in (1 \dots n) ⟼ f (k)) = {f ↾}_{(1 \dots n)}$
217	216	rneqd	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to ran (k \in (1 \dots n) ⟼ f (k)) = ran ({f ↾}_{(1 \dots n)})$
218	197 217	esumeq1d	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to \underset{z \in ran (k \in (1 \dots n) ⟼ f (k))}{\sum^{}} M (z) = \underset{z \in ran ({f ↾}_{(1 \dots n)})}{\sum^{}} M (z)$
219	155	a1i	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to (1 \dots n) \in Fin$
220	23	ad2antrr	$⊢ (((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \land k \in (1 \dots n)) \to M : 𝒫 O ⟶ [0, +∞]$
221	151	a1i	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to (1 \dots n) \subseteq ℕ$
222	221	sselda	$⊢ (((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \land k \in (1 \dots n)) \to k \in ℕ$
223	87	adantlr	$⊢ (((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \land k \in ℕ) \to f (k) \in 𝒫 O$
224	222 223	syldan	$⊢ (((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \land k \in (1 \dots n)) \to f (k) \in 𝒫 O$
225	220 224	ffvelrnd	$⊢ (((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \land k \in (1 \dots n)) \to M (f (k)) \in [0, +∞]$
226		simpr	$⊢ ((((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \land k \in (1 \dots n)) \land f (k) = \emptyset) \to f (k) = \emptyset$
227	226	fveq2d	$⊢ ((((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \land k \in (1 \dots n)) \land f (k) = \emptyset) \to M (f (k)) = M (\emptyset)$
228	24	ad3antrrr	$⊢ ((((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \land k \in (1 \dots n)) \land f (k) = \emptyset) \to M (\emptyset) = 0$
229	227 228	eqtrd	$⊢ ((((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \land k \in (1 \dots n)) \land f (k) = \emptyset) \to M (f (k)) = 0$
230		disjss1	$⊢ (1 \dots n) \subseteq ℕ \to (\underset{k \in ℕ}{Disj} f (k) \to {Disj}_{k = 1}^{n} f (k))$
231	151 230	ax-mp	$⊢ \underset{k \in ℕ}{Disj} f (k) \to {Disj}_{k = 1}^{n} f (k)$
232	133 231	syl	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to {Disj}_{k = 1}^{n} f (k)$
233	232	adantr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to {Disj}_{k = 1}^{n} f (k)$
234	79 219 225 224 229 233	esumrnmpt2	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to \underset{z \in ran (k \in (1 \dots n) ⟼ f (k))}{\sum^{}} M (z) = {\sum^{}}_{k = 1}^{n} M (f (k))$
235	210 218 234	3eqtr2d	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to \underset{z \in ran ({f ↾}_{(1 \dots n)})}{\sum^{}} M (O \cap z) = {\sum^{}}_{k = 1}^{n} M (f (k))$
236	179 196 235	3eqtr3d	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to M (⋃ ran ({f ↾}_{(1 \dots n)})) = {\sum^{*}}_{k = 1}^{n} M (f (k))$
237	9	3adant1r	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land x \subseteq y \land y \in 𝒫 O) \to M (x) \leq M (y)$
238	22 23 186 140 237	carsgmon	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to M (⋃ ran ({f ↾}_{(1 \dots n)})) \leq M (⋃ A)$
239	238	adantr	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to M (⋃ ran ({f ↾}_{(1 \dots n)})) \leq M (⋃ A)$
240	236 239	eqbrtrrd	$⊢ ((φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} M (f (k)) \leq M (⋃ A)$
241	141 88 240	esumgect	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{k \in ℕ}{\sum^{*}} M (f (k)) \leq M (⋃ A)$
242	135 241	eqbrtrrd	$⊢ (φ \land (f : ℕ ⟶ A \cup \{\emptyset\} \land A \subseteq ran f \land Fun ({f^{-1} ↾}_{A}))) \to \underset{z \in A}{\sum^{*}} M (z) \leq M (⋃ A)$
243	13 242	exlimddv	$⊢ φ \to \underset{z \in A}{\sum^{*}} M (z) \leq M (⋃ A)$

Metamath Proof Explorer

Theorem carsggect

Proof