caratheodorylem2

Description: Caratheodory's construction is sigma-additive. Main part of Step (e) in the proof of Theorem 113C of Fremlin1 p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	caratheodorylem2.o	$⊢ φ \to O \in OutMeas$
	caratheodorylem2.x	$⊢ X = ⋃ dom O$
	caratheodorylem2.s	$⊢ S = CaraGen (O)$
	caratheodorylem2.e	$⊢ φ \to E : ℕ ⟶ S$
	caratheodorylem2.5	$⊢ φ \to \underset{n \in ℕ}{Disj} E (n)$
	caratheodorylem2.g	$⊢ G = (k \in ℕ ⟼ ⋃_{n = 1}^{k} E (n))$
Assertion	caratheodorylem2	$⊢ φ \to O (⋃_{n \in ℕ} E (n)) = sum^((n \in ℕ ⟼ O (E (n))))$

Proof

Step	Hyp	Ref	Expression
1		caratheodorylem2.o	$⊢ φ \to O \in OutMeas$
2		caratheodorylem2.x	$⊢ X = ⋃ dom O$
3		caratheodorylem2.s	$⊢ S = CaraGen (O)$
4		caratheodorylem2.e	$⊢ φ \to E : ℕ ⟶ S$
5		caratheodorylem2.5	$⊢ φ \to \underset{n \in ℕ}{Disj} E (n)$
6		caratheodorylem2.g	$⊢ G = (k \in ℕ ⟼ ⋃_{n = 1}^{k} E (n))$
7	3	caragenss	$⊢ O \in OutMeas \to S \subseteq dom O$
8	1 7	syl	$⊢ φ \to S \subseteq dom O$
9	8	adantr	$⊢ (φ \land n \in ℕ) \to S \subseteq dom O$
10	4	ffvelrnda	$⊢ (φ \land n \in ℕ) \to E (n) \in S$
11	9 10	sseldd	$⊢ (φ \land n \in ℕ) \to E (n) \in dom O$
12		elssuni	$⊢ E (n) \in dom O \to E (n) \subseteq ⋃ dom O$
13	11 12	syl	$⊢ (φ \land n \in ℕ) \to E (n) \subseteq ⋃ dom O$
14	13 2	sseqtrrdi	$⊢ (φ \land n \in ℕ) \to E (n) \subseteq X$
15	14	ralrimiva	$⊢ φ \to \forall n \in ℕ E (n) \subseteq X$
16		iunss	$⊢ ⋃_{n \in ℕ} E (n) \subseteq X \leftrightarrow \forall n \in ℕ E (n) \subseteq X$
17	15 16	sylibr	$⊢ φ \to ⋃_{n \in ℕ} E (n) \subseteq X$
18	1 2 17	omexrcl	$⊢ φ \to O (⋃_{n \in ℕ} E (n)) \in ℝ^{*}$
19		nnex	$⊢ ℕ \in V$
20	19	a1i	$⊢ φ \to ℕ \in V$
21	1	adantr	$⊢ (φ \land n \in ℕ) \to O \in OutMeas$
22	21 2 14	omecl	$⊢ (φ \land n \in ℕ) \to O (E (n)) \in [0, +∞]$
23		eqid	$⊢ (n \in ℕ ⟼ O (E (n))) = (n \in ℕ ⟼ O (E (n)))$
24	22 23	fmptd	$⊢ φ \to (n \in ℕ ⟼ O (E (n))) : ℕ ⟶ [0, +∞]$
25	20 24	sge0xrcl	$⊢ φ \to sum^((n \in ℕ ⟼ O (E (n)))) \in ℝ^{*}$
26		nfv	$⊢ Ⅎ n φ$
27		nfcv	$⊢ \underline{Ⅎ} n E$
28		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
29	1 2 3	caragensspw	$⊢ φ \to S \subseteq 𝒫 X$
30	4 29	fssd	$⊢ φ \to E : ℕ ⟶ 𝒫 X$
31	26 27 1 2 28 30	omeiunle	$⊢ φ \to O (⋃_{n \in ℕ} E (n)) \leq sum^((n \in ℕ ⟼ O (E (n))))$
32		elpwinss	$⊢ x \in (𝒫 ℕ \cap Fin) \to x \subseteq ℕ$
33	32	resmptd	$⊢ x \in (𝒫 ℕ \cap Fin) \to {(n \in ℕ ⟼ O (E (n))) ↾}_{x} = (n \in x ⟼ O (E (n)))$
34	33	fveq2d	$⊢ x \in (𝒫 ℕ \cap Fin) \to sum^({(n \in ℕ ⟼ O (E (n))) ↾}_{x}) = sum^((n \in x ⟼ O (E (n))))$
35	34	adantl	$⊢ (φ \land x \in (𝒫 ℕ \cap Fin)) \to sum^({(n \in ℕ ⟼ O (E (n))) ↾}_{x}) = sum^((n \in x ⟼ O (E (n))))$
36		1zzd	$⊢ (φ \land x \in (𝒫 ℕ \cap Fin)) \to 1 \in ℤ$
37	32	adantl	$⊢ (φ \land x \in (𝒫 ℕ \cap Fin)) \to x \subseteq ℕ$
38		elinel2	$⊢ x \in (𝒫 ℕ \cap Fin) \to x \in Fin$
39	38	adantl	$⊢ (φ \land x \in (𝒫 ℕ \cap Fin)) \to x \in Fin$
40	36 28 37 39	uzfissfz	$⊢ (φ \land x \in (𝒫 ℕ \cap Fin)) \to \exists k \in ℕ x \subseteq (1 \dots k)$
41		vex	$⊢ x \in V$
42	41	a1i	$⊢ (φ \land x \subseteq (1 \dots k)) \to x \in V$
43	1	ad2antrr	$⊢ ((φ \land x \subseteq (1 \dots k)) \land n \in x) \to O \in OutMeas$
44	30	ad2antrr	$⊢ ((φ \land x \subseteq (1 \dots k)) \land n \in x) \to E : ℕ ⟶ 𝒫 X$
45		fz1ssnn	$⊢ (1 \dots k) \subseteq ℕ$
46		ssel2	$⊢ (x \subseteq (1 \dots k) \land n \in x) \to n \in (1 \dots k)$
47	45 46	sseldi	$⊢ (x \subseteq (1 \dots k) \land n \in x) \to n \in ℕ$
48	47	adantll	$⊢ ((φ \land x \subseteq (1 \dots k)) \land n \in x) \to n \in ℕ$
49	44 48	ffvelrnd	$⊢ ((φ \land x \subseteq (1 \dots k)) \land n \in x) \to E (n) \in 𝒫 X$
50		elpwi	$⊢ E (n) \in 𝒫 X \to E (n) \subseteq X$
51	49 50	syl	$⊢ ((φ \land x \subseteq (1 \dots k)) \land n \in x) \to E (n) \subseteq X$
52	43 2 51	omecl	$⊢ ((φ \land x \subseteq (1 \dots k)) \land n \in x) \to O (E (n)) \in [0, +∞]$
53		eqid	$⊢ (n \in x ⟼ O (E (n))) = (n \in x ⟼ O (E (n)))$
54	52 53	fmptd	$⊢ (φ \land x \subseteq (1 \dots k)) \to (n \in x ⟼ O (E (n))) : x ⟶ [0, +∞]$
55	42 54	sge0xrcl	$⊢ (φ \land x \subseteq (1 \dots k)) \to sum^((n \in x ⟼ O (E (n)))) \in ℝ^{*}$
56	55	3adant2	$⊢ (φ \land k \in ℕ \land x \subseteq (1 \dots k)) \to sum^((n \in x ⟼ O (E (n)))) \in ℝ^{*}$
57		ovex	$⊢ (1 \dots k) \in V$
58	57	a1i	$⊢ φ \to (1 \dots k) \in V$
59		elfznn	$⊢ n \in (1 \dots k) \to n \in ℕ$
60	59 22	sylan2	$⊢ (φ \land n \in (1 \dots k)) \to O (E (n)) \in [0, +∞]$
61		eqid	$⊢ (n \in (1 \dots k) ⟼ O (E (n))) = (n \in (1 \dots k) ⟼ O (E (n)))$
62	60 61	fmptd	$⊢ φ \to (n \in (1 \dots k) ⟼ O (E (n))) : (1 \dots k) ⟶ [0, +∞]$
63	58 62	sge0xrcl	$⊢ φ \to sum^((n \in (1 \dots k) ⟼ O (E (n)))) \in ℝ^{*}$
64	63	3ad2ant1	$⊢ (φ \land k \in ℕ \land x \subseteq (1 \dots k)) \to sum^((n \in (1 \dots k) ⟼ O (E (n)))) \in ℝ^{*}$
65	18	3ad2ant1	$⊢ (φ \land k \in ℕ \land x \subseteq (1 \dots k)) \to O (⋃_{n \in ℕ} E (n)) \in ℝ^{*}$
66	57	a1i	$⊢ (φ \land k \in ℕ \land x \subseteq (1 \dots k)) \to (1 \dots k) \in V$
67		simpl1	$⊢ ((φ \land k \in ℕ \land x \subseteq (1 \dots k)) \land n \in (1 \dots k)) \to φ$
68	59	adantl	$⊢ ((φ \land k \in ℕ \land x \subseteq (1 \dots k)) \land n \in (1 \dots k)) \to n \in ℕ$
69	67 68 22	syl2anc	$⊢ ((φ \land k \in ℕ \land x \subseteq (1 \dots k)) \land n \in (1 \dots k)) \to O (E (n)) \in [0, +∞]$
70		simp3	$⊢ (φ \land k \in ℕ \land x \subseteq (1 \dots k)) \to x \subseteq (1 \dots k)$
71	66 69 70	sge0lessmpt	$⊢ (φ \land k \in ℕ \land x \subseteq (1 \dots k)) \to sum^((n \in x ⟼ O (E (n)))) \leq sum^((n \in (1 \dots k) ⟼ O (E (n))))$
72	1	adantr	$⊢ (φ \land k \in ℕ) \to O \in OutMeas$
73	4	adantr	$⊢ (φ \land k \in ℕ) \to E : ℕ ⟶ S$
74	5	adantr	$⊢ (φ \land k \in ℕ) \to \underset{n \in ℕ}{Disj} E (n)$
75		nfiu1	$⊢ \underline{Ⅎ} n ⋃_{n = 1}^{k} E (n)$
76		nfcv	$⊢ \underline{Ⅎ} k ⋃_{m = 1}^{n} E (m)$
77		fveq2	$⊢ n = m \to E (n) = E (m)$
78	77	cbviunv	$⊢ ⋃_{n = 1}^{k} E (n) = ⋃_{m = 1}^{k} E (m)$
79	78	a1i	$⊢ k = n \to ⋃_{n = 1}^{k} E (n) = ⋃_{m = 1}^{k} E (m)$
80		oveq2	$⊢ k = n \to (1 \dots k) = (1 \dots n)$
81	80	iuneq1d	$⊢ k = n \to ⋃_{m = 1}^{k} E (m) = ⋃_{m = 1}^{n} E (m)$
82	79 81	eqtrd	$⊢ k = n \to ⋃_{n = 1}^{k} E (n) = ⋃_{m = 1}^{n} E (m)$
83	75 76 82	cbvmpt	$⊢ (k \in ℕ ⟼ ⋃_{n = 1}^{k} E (n)) = (n \in ℕ ⟼ ⋃_{m = 1}^{n} E (m))$
84	6 83	eqtri	$⊢ G = (n \in ℕ ⟼ ⋃_{m = 1}^{n} E (m))$
85		id	$⊢ k \in ℕ \to k \in ℕ$
86	85 28	eleqtrdi	$⊢ k \in ℕ \to k \in ℤ_{\geq 1}$
87	86	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℤ_{\geq 1}$
88	72 3 28 73 74 84 87	caratheodorylem1	$⊢ (φ \land k \in ℕ) \to O (G (k)) = sum^((n \in (1 \dots k) ⟼ O (E (n))))$
89	88	eqcomd	$⊢ (φ \land k \in ℕ) \to sum^((n \in (1 \dots k) ⟼ O (E (n)))) = O (G (k))$
90	17	adantr	$⊢ (φ \land k \in ℕ) \to ⋃_{n \in ℕ} E (n) \subseteq X$
91		fvex	$⊢ E (n) \in V$
92	57 91	iunex	$⊢ ⋃_{n = 1}^{k} E (n) \in V$
93	6	fvmpt2	$⊢ (k \in ℕ \land ⋃_{n = 1}^{k} E (n) \in V) \to G (k) = ⋃_{n = 1}^{k} E (n)$
94	85 92 93	sylancl	$⊢ k \in ℕ \to G (k) = ⋃_{n = 1}^{k} E (n)$
95	45	a1i	$⊢ k \in ℕ \to (1 \dots k) \subseteq ℕ$
96		iunss1	$⊢ (1 \dots k) \subseteq ℕ \to ⋃_{n = 1}^{k} E (n) \subseteq ⋃_{n \in ℕ} E (n)$
97	95 96	syl	$⊢ k \in ℕ \to ⋃_{n = 1}^{k} E (n) \subseteq ⋃_{n \in ℕ} E (n)$
98	94 97	eqsstrd	$⊢ k \in ℕ \to G (k) \subseteq ⋃_{n \in ℕ} E (n)$
99	98	adantl	$⊢ (φ \land k \in ℕ) \to G (k) \subseteq ⋃_{n \in ℕ} E (n)$
100	72 2 90 99	omessle	$⊢ (φ \land k \in ℕ) \to O (G (k)) \leq O (⋃_{n \in ℕ} E (n))$
101	89 100	eqbrtrd	$⊢ (φ \land k \in ℕ) \to sum^((n \in (1 \dots k) ⟼ O (E (n)))) \leq O (⋃_{n \in ℕ} E (n))$
102	101	3adant3	$⊢ (φ \land k \in ℕ \land x \subseteq (1 \dots k)) \to sum^((n \in (1 \dots k) ⟼ O (E (n)))) \leq O (⋃_{n \in ℕ} E (n))$
103	56 64 65 71 102	xrletrd	$⊢ (φ \land k \in ℕ \land x \subseteq (1 \dots k)) \to sum^((n \in x ⟼ O (E (n)))) \leq O (⋃_{n \in ℕ} E (n))$
104	103	3exp	$⊢ φ \to (k \in ℕ \to (x \subseteq (1 \dots k) \to sum^((n \in x ⟼ O (E (n)))) \leq O (⋃_{n \in ℕ} E (n))))$
105	104	adantr	$⊢ (φ \land x \in (𝒫 ℕ \cap Fin)) \to (k \in ℕ \to (x \subseteq (1 \dots k) \to sum^((n \in x ⟼ O (E (n)))) \leq O (⋃_{n \in ℕ} E (n))))$
106	105	rexlimdv	$⊢ (φ \land x \in (𝒫 ℕ \cap Fin)) \to (\exists k \in ℕ x \subseteq (1 \dots k) \to sum^((n \in x ⟼ O (E (n)))) \leq O (⋃_{n \in ℕ} E (n)))$
107	40 106	mpd	$⊢ (φ \land x \in (𝒫 ℕ \cap Fin)) \to sum^((n \in x ⟼ O (E (n)))) \leq O (⋃_{n \in ℕ} E (n))$
108	35 107	eqbrtrd	$⊢ (φ \land x \in (𝒫 ℕ \cap Fin)) \to sum^({(n \in ℕ ⟼ O (E (n))) ↾}_{x}) \leq O (⋃_{n \in ℕ} E (n))$
109	108	ralrimiva	$⊢ φ \to \forall x \in (𝒫 ℕ \cap Fin) sum^({(n \in ℕ ⟼ O (E (n))) ↾}_{x}) \leq O (⋃_{n \in ℕ} E (n))$
110	20 24 18	sge0lefi	$⊢ φ \to (sum^((n \in ℕ ⟼ O (E (n)))) \leq O (⋃_{n \in ℕ} E (n)) \leftrightarrow \forall x \in (𝒫 ℕ \cap Fin) sum^({(n \in ℕ ⟼ O (E (n))) ↾}_{x}) \leq O (⋃_{n \in ℕ} E (n)))$
111	109 110	mpbird	$⊢ φ \to sum^((n \in ℕ ⟼ O (E (n)))) \leq O (⋃_{n \in ℕ} E (n))$
112	18 25 31 111	xrletrid	$⊢ φ \to O (⋃_{n \in ℕ} E (n)) = sum^((n \in ℕ ⟼ O (E (n))))$

Metamath Proof Explorer

Theorem caratheodorylem2

Proof