carageniuncl

Description: The Caratheodory's construction is closed under indexed countable union. Step (d) in the proof of Theorem 113C of Fremlin1 p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	carageniuncl.o	$⊢ φ \to O \in OutMeas$
	carageniuncl.s	$⊢ S = CaraGen (O)$
	carageniuncl.3	$⊢ φ \to M \in ℤ$
	carageniuncl.z	$⊢ Z = ℤ_{\geq M}$
	carageniuncl.e	$⊢ φ \to E : Z ⟶ S$
Assertion	carageniuncl	$⊢ φ \to ⋃_{n \in Z} E (n) \in S$

Proof

Step	Hyp	Ref	Expression
1		carageniuncl.o	$⊢ φ \to O \in OutMeas$
2		carageniuncl.s	$⊢ S = CaraGen (O)$
3		carageniuncl.3	$⊢ φ \to M \in ℤ$
4		carageniuncl.z	$⊢ Z = ℤ_{\geq M}$
5		carageniuncl.e	$⊢ φ \to E : Z ⟶ S$
6		eqid	$⊢ ⋃ dom O = ⋃ dom O$
7	5	ffvelcdmda	$⊢ (φ \land n \in Z) \to E (n) \in S$
8		elssuni	$⊢ E (n) \in S \to E (n) \subseteq ⋃ S$
9	7 8	syl	$⊢ (φ \land n \in Z) \to E (n) \subseteq ⋃ S$
10	1 2	caragenuni	$⊢ φ \to ⋃ S = ⋃ dom O$
11	10	adantr	$⊢ (φ \land n \in Z) \to ⋃ S = ⋃ dom O$
12	9 11	sseqtrd	$⊢ (φ \land n \in Z) \to E (n) \subseteq ⋃ dom O$
13	12	ralrimiva	$⊢ φ \to \forall n \in Z E (n) \subseteq ⋃ dom O$
14		iunss	$⊢ ⋃_{n \in Z} E (n) \subseteq ⋃ dom O \leftrightarrow \forall n \in Z E (n) \subseteq ⋃ dom O$
15	13 14	sylibr	$⊢ φ \to ⋃_{n \in Z} E (n) \subseteq ⋃ dom O$
16	4	fvexi	$⊢ Z \in V$
17		fvex	$⊢ E (n) \in V$
18	16 17	iunex	$⊢ ⋃_{n \in Z} E (n) \in V$
19	18	a1i	$⊢ φ \to ⋃_{n \in Z} E (n) \in V$
20		elpwg	$⊢ ⋃_{n \in Z} E (n) \in V \to (⋃_{n \in Z} E (n) \in 𝒫 ⋃ dom O \leftrightarrow ⋃_{n \in Z} E (n) \subseteq ⋃ dom O)$
21	19 20	syl	$⊢ φ \to (⋃_{n \in Z} E (n) \in 𝒫 ⋃ dom O \leftrightarrow ⋃_{n \in Z} E (n) \subseteq ⋃ dom O)$
22	15 21	mpbird	$⊢ φ \to ⋃_{n \in Z} E (n) \in 𝒫 ⋃ dom O$
23		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
24	1	adantr	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O \in OutMeas$
25		elpwi	$⊢ a \in 𝒫 ⋃ dom O \to a \subseteq ⋃ dom O$
26		ssinss1	$⊢ a \subseteq ⋃ dom O \to a \cap ⋃_{n \in Z} E (n) \subseteq ⋃ dom O$
27	25 26	syl	$⊢ a \in 𝒫 ⋃ dom O \to a \cap ⋃_{n \in Z} E (n) \subseteq ⋃ dom O$
28	27	adantl	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to a \cap ⋃_{n \in Z} E (n) \subseteq ⋃ dom O$
29	24 6 28	omecl	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a \cap ⋃_{n \in Z} E (n)) \in [0, +∞]$
30	23 29	sselid	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a \cap ⋃_{n \in Z} E (n)) \in ℝ^{*}$
31	25	adantl	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to a \subseteq ⋃ dom O$
32	31	ssdifssd	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to a ∖ ⋃_{n \in Z} E (n) \subseteq ⋃ dom O$
33	24 6 32	omecl	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a ∖ ⋃_{n \in Z} E (n)) \in [0, +∞]$
34	23 33	sselid	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a ∖ ⋃_{n \in Z} E (n)) \in ℝ^{*}$
35	30 34	xaddcld	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \in ℝ^{*}$
36	24 6 31	omecl	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a) \in [0, +∞]$
37	23 36	sselid	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a) \in ℝ^{*}$
38		pnfge	$⊢ O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \in ℝ^{*} \to O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \leq +∞$
39	35 38	syl	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \leq +∞$
40	39	adantr	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land O (a) = +∞) \to O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \leq +∞$
41		id	$⊢ O (a) = +∞ \to O (a) = +∞$
42	41	eqcomd	$⊢ O (a) = +∞ \to +∞ = O (a)$
43	42	adantl	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land O (a) = +∞) \to +∞ = O (a)$
44	40 43	breqtrd	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land O (a) = +∞) \to O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \leq O (a)$
45		simpl	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land \neg O (a) = +∞) \to (φ \land a \in 𝒫 ⋃ dom O)$
46		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
47		0xr	$⊢ 0 \in ℝ^{*}$
48	47	a1i	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land \neg O (a) = +∞) \to 0 \in ℝ^{*}$
49		pnfxr	$⊢ +∞ \in ℝ^{*}$
50	49	a1i	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land \neg O (a) = +∞) \to +∞ \in ℝ^{*}$
51	45 36	syl	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land \neg O (a) = +∞) \to O (a) \in [0, +∞]$
52	41	necon3bi	$⊢ \neg O (a) = +∞ \to O (a) \neq +∞$
53	52	adantl	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land \neg O (a) = +∞) \to O (a) \neq +∞$
54	48 50 51 53	eliccelicod	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land \neg O (a) = +∞) \to O (a) \in [0, +∞)$
55	46 54	sselid	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land \neg O (a) = +∞) \to O (a) \in ℝ$
56	24	ad2antrr	$⊢ (((φ \land a \in 𝒫 ⋃ dom O) \land O (a) \in ℝ) \land x \in ℝ^{+}) \to O \in OutMeas$
57	31	ad2antrr	$⊢ (((φ \land a \in 𝒫 ⋃ dom O) \land O (a) \in ℝ) \land x \in ℝ^{+}) \to a \subseteq ⋃ dom O$
58		simpr	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land O (a) \in ℝ) \to O (a) \in ℝ$
59	58	adantr	$⊢ (((φ \land a \in 𝒫 ⋃ dom O) \land O (a) \in ℝ) \land x \in ℝ^{+}) \to O (a) \in ℝ$
60	3	ad3antrrr	$⊢ (((φ \land a \in 𝒫 ⋃ dom O) \land O (a) \in ℝ) \land x \in ℝ^{+}) \to M \in ℤ$
61	5	ad3antrrr	$⊢ (((φ \land a \in 𝒫 ⋃ dom O) \land O (a) \in ℝ) \land x \in ℝ^{+}) \to E : Z ⟶ S$
62		simpr	$⊢ (((φ \land a \in 𝒫 ⋃ dom O) \land O (a) \in ℝ) \land x \in ℝ^{+}) \to x \in ℝ^{+}$
63		eqid	$⊢ (n \in Z ⟼ ⋃_{i = M}^{n} E (i)) = (n \in Z ⟼ ⋃_{i = M}^{n} E (i))$
64		fveq2	$⊢ m = n \to E (m) = E (n)$
65		oveq2	$⊢ m = n \to (M ..^m) = (M ..^n)$
66	65	iuneq1d	$⊢ m = n \to ⋃_{i \in (M ..^m)} E (i) = ⋃_{i \in (M ..^n)} E (i)$
67	64 66	difeq12d	$⊢ m = n \to E (m) ∖ ⋃_{i \in (M ..^m)} E (i) = E (n) ∖ ⋃_{i \in (M ..^n)} E (i)$
68	67	cbvmptv	$⊢ (m \in Z ⟼ E (m) ∖ ⋃_{i \in (M ..^m)} E (i)) = (n \in Z ⟼ E (n) ∖ ⋃_{i \in (M ..^n)} E (i))$
69	56 2 6 57 59 60 4 61 62 63 68	carageniuncllem2	$⊢ (((φ \land a \in 𝒫 ⋃ dom O) \land O (a) \in ℝ) \land x \in ℝ^{+}) \to O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \leq O (a) + x$
70	69	ralrimiva	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land O (a) \in ℝ) \to \forall x \in ℝ^{+} O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \leq O (a) + x$
71	35	adantr	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land O (a) \in ℝ) \to O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \in ℝ^{*}$
72		xralrple	$⊢ (O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \in ℝ^{*} \land O (a) \in ℝ) \to (O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \leq O (a) \leftrightarrow \forall x \in ℝ^{+} O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \leq O (a) + x)$
73	71 58 72	syl2anc	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land O (a) \in ℝ) \to (O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \leq O (a) \leftrightarrow \forall x \in ℝ^{+} O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \leq O (a) + x)$
74	70 73	mpbird	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land O (a) \in ℝ) \to O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \leq O (a)$
75	45 55 74	syl2anc	$⊢ ((φ \land a \in 𝒫 ⋃ dom O) \land \neg O (a) = +∞) \to O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \leq O (a)$
76	44 75	pm2.61dan	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) \leq O (a)$
77	24 6 31	omelesplit	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a) \leq O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n))$
78	35 37 76 77	xrletrid	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (a ∖ ⋃_{n \in Z} E (n)) = O (a)$
79	1 6 2 22 78	carageneld	$⊢ φ \to ⋃_{n \in Z} E (n) \in S$

Metamath Proof Explorer

Theorem carageniuncl

Proof