meaiuninc3v

Description: Measures are continuous from below: if E is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is the general case of Proposition 112C (e) of Fremlin1 p. 16 . This theorem generalizes meaiuninc and meaiuninc2 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022)

	Ref	Expression
Hypotheses	meaiuninc3v.m	$⊢ φ \to M \in Meas$
	meaiuninc3v.n	$⊢ φ \to N \in ℤ$
	meaiuninc3v.z	$⊢ Z = ℤ_{\geq N}$
	meaiuninc3v.e	$⊢ φ \to E : Z ⟶ dom M$
	meaiuninc3v.i	$⊢ (φ \land n \in Z) \to E (n) \subseteq E (n + 1)$
	meaiuninc3v.s	$⊢ S = (n \in Z ⟼ M (E (n)))$
Assertion	meaiuninc3v	$⊢ φ \to S \underset{*}{⇝} M (⋃_{n \in Z} E (n))$

Proof

Step	Hyp	Ref	Expression
1		meaiuninc3v.m	$⊢ φ \to M \in Meas$
2		meaiuninc3v.n	$⊢ φ \to N \in ℤ$
3		meaiuninc3v.z	$⊢ Z = ℤ_{\geq N}$
4		meaiuninc3v.e	$⊢ φ \to E : Z ⟶ dom M$
5		meaiuninc3v.i	$⊢ (φ \land n \in Z) \to E (n) \subseteq E (n + 1)$
6		meaiuninc3v.s	$⊢ S = (n \in Z ⟼ M (E (n)))$
7	2	adantr	$⊢ (φ \land \exists x \in ℝ \forall n \in Z M (E (n)) \leq x) \to N \in ℤ$
8	1	adantr	$⊢ (φ \land n \in Z) \to M \in Meas$
9		eqid	$⊢ dom M = dom M$
10	4	ffvelcdmda	$⊢ (φ \land n \in Z) \to E (n) \in dom M$
11	8 9 10	meaxrcl	$⊢ (φ \land n \in Z) \to M (E (n)) \in ℝ^{*}$
12	11 6	fmptd	$⊢ φ \to S : Z ⟶ ℝ^{*}$
13	12	adantr	$⊢ (φ \land \exists x \in ℝ \forall n \in Z M (E (n)) \leq x) \to S : Z ⟶ ℝ^{*}$
14		nfv	$⊢ Ⅎ n φ$
15		nfcv	$⊢ \underline{Ⅎ} n ℝ$
16		nfra1	$⊢ Ⅎ n \forall n \in Z M (E (n)) \leq x$
17	15 16	nfrexw	$⊢ Ⅎ n \exists x \in ℝ \forall n \in Z M (E (n)) \leq x$
18	14 17	nfan	$⊢ Ⅎ n (φ \land \exists x \in ℝ \forall n \in Z M (E (n)) \leq x)$
19		nfcv	$⊢ \underline{Ⅎ} n E$
20	1	adantr	$⊢ (φ \land \exists x \in ℝ \forall n \in Z M (E (n)) \leq x) \to M \in Meas$
21	4	adantr	$⊢ (φ \land \exists x \in ℝ \forall n \in Z M (E (n)) \leq x) \to E : Z ⟶ dom M$
22	5	adantlr	$⊢ ((φ \land \exists x \in ℝ \forall n \in Z M (E (n)) \leq x) \land n \in Z) \to E (n) \subseteq E (n + 1)$
23		simpr	$⊢ (φ \land \exists x \in ℝ \forall n \in Z M (E (n)) \leq x) \to \exists x \in ℝ \forall n \in Z M (E (n)) \leq x$
24	18 19 20 7 3 21 22 23 6	meaiunincf	$⊢ (φ \land \exists x \in ℝ \forall n \in Z M (E (n)) \leq x) \to S ⇝ M (⋃_{n \in Z} E (n))$
25	7 3 13 24	climxlim2	$⊢ (φ \land \exists x \in ℝ \forall n \in Z M (E (n)) \leq x) \to S \underset{*}{⇝} M (⋃_{n \in Z} E (n))$
26		simpr	$⊢ (φ \land \neg \exists x \in ℝ \forall n \in Z M (E (n)) \leq x) \to \neg \exists x \in ℝ \forall n \in Z M (E (n)) \leq x$
27		2fveq3	$⊢ j = n \to M (E (j)) = M (E (n))$
28	27	breq2d	$⊢ j = n \to (x < M (E (j)) \leftrightarrow x < M (E (n)))$
29	28	cbvrexvw	$⊢ \exists j \in Z x < M (E (j)) \leftrightarrow \exists n \in Z x < M (E (n))$
30	29	a1i	$⊢ (φ \land x \in ℝ) \to (\exists j \in Z x < M (E (j)) \leftrightarrow \exists n \in Z x < M (E (n)))$
31		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
32	31	ad2antlr	$⊢ ((φ \land x \in ℝ) \land n \in Z) \to x \in ℝ^{*}$
33	11	adantlr	$⊢ ((φ \land x \in ℝ) \land n \in Z) \to M (E (n)) \in ℝ^{*}$
34	32 33	xrltnled	$⊢ ((φ \land x \in ℝ) \land n \in Z) \to (x < M (E (n)) \leftrightarrow \neg M (E (n)) \leq x)$
35	34	rexbidva	$⊢ (φ \land x \in ℝ) \to (\exists n \in Z x < M (E (n)) \leftrightarrow \exists n \in Z \neg M (E (n)) \leq x)$
36	30 35	bitrd	$⊢ (φ \land x \in ℝ) \to (\exists j \in Z x < M (E (j)) \leftrightarrow \exists n \in Z \neg M (E (n)) \leq x)$
37	36	ralbidva	$⊢ φ \to (\forall x \in ℝ \exists j \in Z x < M (E (j)) \leftrightarrow \forall x \in ℝ \exists n \in Z \neg M (E (n)) \leq x)$
38		rexnal	$⊢ \exists n \in Z \neg M (E (n)) \leq x \leftrightarrow \neg \forall n \in Z M (E (n)) \leq x$
39	38	ralbii	$⊢ \forall x \in ℝ \exists n \in Z \neg M (E (n)) \leq x \leftrightarrow \forall x \in ℝ \neg \forall n \in Z M (E (n)) \leq x$
40		ralnex	$⊢ \forall x \in ℝ \neg \forall n \in Z M (E (n)) \leq x \leftrightarrow \neg \exists x \in ℝ \forall n \in Z M (E (n)) \leq x$
41	39 40	bitri	$⊢ \forall x \in ℝ \exists n \in Z \neg M (E (n)) \leq x \leftrightarrow \neg \exists x \in ℝ \forall n \in Z M (E (n)) \leq x$
42	41	a1i	$⊢ φ \to (\forall x \in ℝ \exists n \in Z \neg M (E (n)) \leq x \leftrightarrow \neg \exists x \in ℝ \forall n \in Z M (E (n)) \leq x)$
43	37 42	bitrd	$⊢ φ \to (\forall x \in ℝ \exists j \in Z x < M (E (j)) \leftrightarrow \neg \exists x \in ℝ \forall n \in Z M (E (n)) \leq x)$
44	43	adantr	$⊢ (φ \land \neg \exists x \in ℝ \forall n \in Z M (E (n)) \leq x) \to (\forall x \in ℝ \exists j \in Z x < M (E (j)) \leftrightarrow \neg \exists x \in ℝ \forall n \in Z M (E (n)) \leq x)$
45	26 44	mpbird	$⊢ (φ \land \neg \exists x \in ℝ \forall n \in Z M (E (n)) \leq x) \to \forall x \in ℝ \exists j \in Z x < M (E (j))$
46		simpr	$⊢ (φ \land \forall x \in ℝ \exists j \in Z x < M (E (j))) \to \forall x \in ℝ \exists j \in Z x < M (E (j))$
47	45 46	syldan	$⊢ (φ \land \neg \exists x \in ℝ \forall n \in Z M (E (n)) \leq x) \to \forall x \in ℝ \exists j \in Z x < M (E (j))$
48		simp-4r	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \land n \in ℤ_{\geq j}) \to x \in ℝ$
49	48 31	syl	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \land n \in ℤ_{\geq j}) \to x \in ℝ^{*}$
50		simp-4l	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \land n \in ℤ_{\geq j}) \to φ$
51	3	uztrn2	$⊢ (j \in Z \land n \in ℤ_{\geq j}) \to n \in Z$
52	51	ad4ant24	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \land n \in ℤ_{\geq j}) \to n \in Z$
53	12	ffvelcdmda	$⊢ (φ \land n \in Z) \to S (n) \in ℝ^{*}$
54	50 52 53	syl2anc	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \land n \in ℤ_{\geq j}) \to S (n) \in ℝ^{*}$
55		eleq1w	$⊢ n = j \to (n \in Z \leftrightarrow j \in Z)$
56	55	anbi2d	$⊢ n = j \to ((φ \land n \in Z) \leftrightarrow (φ \land j \in Z))$
57		2fveq3	$⊢ n = j \to M (E (n)) = M (E (j))$
58	57	eleq1d	$⊢ n = j \to (M (E (n)) \in ℝ^{} \leftrightarrow M (E (j)) \in ℝ^{})$
59	56 58	imbi12d	$⊢ n = j \to (((φ \land n \in Z) \to M (E (n)) \in ℝ^{}) \leftrightarrow ((φ \land j \in Z) \to M (E (j)) \in ℝ^{}))$
60	59 11	chvarvv	$⊢ (φ \land j \in Z) \to M (E (j)) \in ℝ^{*}$
61	60	ad5ant13	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \land n \in ℤ_{\geq j}) \to M (E (j)) \in ℝ^{*}$
62		simplr	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \land n \in ℤ_{\geq j}) \to x < M (E (j))$
63	1	3ad2ant1	$⊢ (φ \land j \in Z \land n \in ℤ_{\geq j}) \to M \in Meas$
64	4	ffvelcdmda	$⊢ (φ \land j \in Z) \to E (j) \in dom M$
65	64	3adant3	$⊢ (φ \land j \in Z \land n \in ℤ_{\geq j}) \to E (j) \in dom M$
66		simp1	$⊢ (φ \land j \in Z \land n \in ℤ_{\geq j}) \to φ$
67	51	3adant1	$⊢ (φ \land j \in Z \land n \in ℤ_{\geq j}) \to n \in Z$
68	66 67 10	syl2anc	$⊢ (φ \land j \in Z \land n \in ℤ_{\geq j}) \to E (n) \in dom M$
69		simp3	$⊢ (φ \land j \in Z \land n \in ℤ_{\geq j}) \to n \in ℤ_{\geq j}$
70		simpll	$⊢ ((φ \land j \in Z) \land k \in (j ..^n)) \to φ$
71	3	uzssd3	$⊢ j \in Z \to ℤ_{\geq j} \subseteq Z$
72	71	adantr	$⊢ (j \in Z \land k \in (j ..^n)) \to ℤ_{\geq j} \subseteq Z$
73		elfzouz	$⊢ k \in (j ..^n) \to k \in ℤ_{\geq j}$
74	73	adantl	$⊢ (j \in Z \land k \in (j ..^n)) \to k \in ℤ_{\geq j}$
75	72 74	sseldd	$⊢ (j \in Z \land k \in (j ..^n)) \to k \in Z$
76	75	adantll	$⊢ ((φ \land j \in Z) \land k \in (j ..^n)) \to k \in Z$
77		eleq1w	$⊢ n = k \to (n \in Z \leftrightarrow k \in Z)$
78	77	anbi2d	$⊢ n = k \to ((φ \land n \in Z) \leftrightarrow (φ \land k \in Z))$
79		fveq2	$⊢ n = k \to E (n) = E (k)$
80		fvoveq1	$⊢ n = k \to E (n + 1) = E (k + 1)$
81	79 80	sseq12d	$⊢ n = k \to (E (n) \subseteq E (n + 1) \leftrightarrow E (k) \subseteq E (k + 1))$
82	78 81	imbi12d	$⊢ n = k \to (((φ \land n \in Z) \to E (n) \subseteq E (n + 1)) \leftrightarrow ((φ \land k \in Z) \to E (k) \subseteq E (k + 1)))$
83	82 5	chvarvv	$⊢ (φ \land k \in Z) \to E (k) \subseteq E (k + 1)$
84	70 76 83	syl2anc	$⊢ ((φ \land j \in Z) \land k \in (j ..^n)) \to E (k) \subseteq E (k + 1)$
85	84	3adantl3	$⊢ ((φ \land j \in Z \land n \in ℤ_{\geq j}) \land k \in (j ..^n)) \to E (k) \subseteq E (k + 1)$
86	69 85	ssinc	$⊢ (φ \land j \in Z \land n \in ℤ_{\geq j}) \to E (j) \subseteq E (n)$
87	63 9 65 68 86	meassle	$⊢ (φ \land j \in Z \land n \in ℤ_{\geq j}) \to M (E (j)) \leq M (E (n))$
88		fvexd	$⊢ (j \in Z \land n \in ℤ_{\geq j}) \to M (E (n)) \in V$
89	6	fvmpt2	$⊢ (n \in Z \land M (E (n)) \in V) \to S (n) = M (E (n))$
90	51 88 89	syl2anc	$⊢ (j \in Z \land n \in ℤ_{\geq j}) \to S (n) = M (E (n))$
91	90	3adant1	$⊢ (φ \land j \in Z \land n \in ℤ_{\geq j}) \to S (n) = M (E (n))$
92	87 91	breqtrrd	$⊢ (φ \land j \in Z \land n \in ℤ_{\geq j}) \to M (E (j)) \leq S (n)$
93	92	ad5ant135	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \land n \in ℤ_{\geq j}) \to M (E (j)) \leq S (n)$
94	49 61 54 62 93	xrltletrd	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \land n \in ℤ_{\geq j}) \to x < S (n)$
95	49 54 94	xrltled	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \land n \in ℤ_{\geq j}) \to x \leq S (n)$
96	95	ralrimiva	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \to \forall n \in ℤ_{\geq j} x \leq S (n)$
97	96	ex	$⊢ ((φ \land x \in ℝ) \land j \in Z) \to (x < M (E (j)) \to \forall n \in ℤ_{\geq j} x \leq S (n))$
98	97	reximdva	$⊢ (φ \land x \in ℝ) \to (\exists j \in Z x < M (E (j)) \to \exists j \in Z \forall n \in ℤ_{\geq j} x \leq S (n))$
99	98	ralimdva	$⊢ φ \to (\forall x \in ℝ \exists j \in Z x < M (E (j)) \to \forall x \in ℝ \exists j \in Z \forall n \in ℤ_{\geq j} x \leq S (n))$
100	99	imp	$⊢ (φ \land \forall x \in ℝ \exists j \in Z x < M (E (j))) \to \forall x \in ℝ \exists j \in Z \forall n \in ℤ_{\geq j} x \leq S (n)$
101		nfmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ M (E (n)))$
102	6 101	nfcxfr	$⊢ \underline{Ⅎ} n S$
103	102 2 3 12	xlimpnf	$⊢ φ \to (S \underset{*}{⇝} +∞ \leftrightarrow \forall x \in ℝ \exists j \in Z \forall n \in ℤ_{\geq j} x \leq S (n))$
104	103	adantr	$⊢ (φ \land \forall x \in ℝ \exists j \in Z x < M (E (j))) \to (S \underset{*}{⇝} +∞ \leftrightarrow \forall x \in ℝ \exists j \in Z \forall n \in ℤ_{\geq j} x \leq S (n))$
105	100 104	mpbird	$⊢ (φ \land \forall x \in ℝ \exists j \in Z x < M (E (j))) \to S \underset{*}{⇝} +∞$
106		nfv	$⊢ Ⅎ x φ$
107		nfra1	$⊢ Ⅎ x \forall x \in ℝ \exists j \in Z x < M (E (j))$
108	106 107	nfan	$⊢ Ⅎ x (φ \land \forall x \in ℝ \exists j \in Z x < M (E (j)))$
109		rspa	$⊢ (\forall x \in ℝ \exists j \in Z x < M (E (j)) \land x \in ℝ) \to \exists j \in Z x < M (E (j))$
110	109	adantll	$⊢ ((φ \land \forall x \in ℝ \exists j \in Z x < M (E (j))) \land x \in ℝ) \to \exists j \in Z x < M (E (j))$
111		nfv	$⊢ Ⅎ j φ$
112		nfcv	$⊢ \underline{Ⅎ} j ℝ$
113		nfre1	$⊢ Ⅎ j \exists j \in Z x < M (E (j))$
114	112 113	nfralw	$⊢ Ⅎ j \forall x \in ℝ \exists j \in Z x < M (E (j))$
115	111 114	nfan	$⊢ Ⅎ j (φ \land \forall x \in ℝ \exists j \in Z x < M (E (j)))$
116		nfv	$⊢ Ⅎ j x \in ℝ$
117	115 116	nfan	$⊢ Ⅎ j ((φ \land \forall x \in ℝ \exists j \in Z x < M (E (j))) \land x \in ℝ)$
118		nfv	$⊢ Ⅎ j x \leq M (⋃_{n \in Z} E (n))$
119	31	ad3antlr	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \to x \in ℝ^{*}$
120	1 9	dmmeasal	$⊢ φ \to dom M \in SAlg$
121	3	uzct	$⊢ Z ≼ ω$
122	121	a1i	$⊢ φ \to Z ≼ ω$
123	120 122 10	saliuncl	$⊢ φ \to ⋃_{n \in Z} E (n) \in dom M$
124	1 9 123	meaxrcl	$⊢ φ \to M (⋃_{n \in Z} E (n)) \in ℝ^{*}$
125	124	ad3antrrr	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \to M (⋃_{n \in Z} E (n)) \in ℝ^{*}$
126	60	ad4ant13	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \to M (E (j)) \in ℝ^{*}$
127		simpr	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \to x < M (E (j))$
128	1	adantr	$⊢ (φ \land j \in Z) \to M \in Meas$
129	123	adantr	$⊢ (φ \land j \in Z) \to ⋃_{n \in Z} E (n) \in dom M$
130		fveq2	$⊢ n = j \to E (n) = E (j)$
131	130	ssiun2s	$⊢ j \in Z \to E (j) \subseteq ⋃_{n \in Z} E (n)$
132	131	adantl	$⊢ (φ \land j \in Z) \to E (j) \subseteq ⋃_{n \in Z} E (n)$
133	128 9 64 129 132	meassle	$⊢ (φ \land j \in Z) \to M (E (j)) \leq M (⋃_{n \in Z} E (n))$
134	133	ad4ant13	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \to M (E (j)) \leq M (⋃_{n \in Z} E (n))$
135	119 126 125 127 134	xrltletrd	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \to x < M (⋃_{n \in Z} E (n))$
136	119 125 135	xrltled	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land x < M (E (j))) \to x \leq M (⋃_{n \in Z} E (n))$
137	136	exp31	$⊢ (φ \land x \in ℝ) \to (j \in Z \to (x < M (E (j)) \to x \leq M (⋃_{n \in Z} E (n))))$
138	137	adantlr	$⊢ ((φ \land \forall x \in ℝ \exists j \in Z x < M (E (j))) \land x \in ℝ) \to (j \in Z \to (x < M (E (j)) \to x \leq M (⋃_{n \in Z} E (n))))$
139	117 118 138	rexlimd	$⊢ ((φ \land \forall x \in ℝ \exists j \in Z x < M (E (j))) \land x \in ℝ) \to (\exists j \in Z x < M (E (j)) \to x \leq M (⋃_{n \in Z} E (n)))$
140	110 139	mpd	$⊢ ((φ \land \forall x \in ℝ \exists j \in Z x < M (E (j))) \land x \in ℝ) \to x \leq M (⋃_{n \in Z} E (n))$
141	108 140	ralrimia	$⊢ (φ \land \forall x \in ℝ \exists j \in Z x < M (E (j))) \to \forall x \in ℝ x \leq M (⋃_{n \in Z} E (n))$
142		xrpnf	$⊢ M (⋃_{n \in Z} E (n)) \in ℝ^{*} \to (M (⋃_{n \in Z} E (n)) = +∞ \leftrightarrow \forall x \in ℝ x \leq M (⋃_{n \in Z} E (n)))$
143	124 142	syl	$⊢ φ \to (M (⋃_{n \in Z} E (n)) = +∞ \leftrightarrow \forall x \in ℝ x \leq M (⋃_{n \in Z} E (n)))$
144	143	adantr	$⊢ (φ \land \forall x \in ℝ \exists j \in Z x < M (E (j))) \to (M (⋃_{n \in Z} E (n)) = +∞ \leftrightarrow \forall x \in ℝ x \leq M (⋃_{n \in Z} E (n)))$
145	141 144	mpbird	$⊢ (φ \land \forall x \in ℝ \exists j \in Z x < M (E (j))) \to M (⋃_{n \in Z} E (n)) = +∞$
146	105 145	breqtrrd	$⊢ (φ \land \forall x \in ℝ \exists j \in Z x < M (E (j))) \to S \underset{*}{⇝} M (⋃_{n \in Z} E (n))$
147	47 146	syldan	$⊢ (φ \land \neg \exists x \in ℝ \forall n \in Z M (E (n)) \leq x) \to S \underset{*}{⇝} M (⋃_{n \in Z} E (n))$
148	25 147	pm2.61dan	$⊢ φ \to S \underset{*}{⇝} M (⋃_{n \in Z} E (n))$

Metamath Proof Explorer

Theorem meaiuninc3v

Proof