voliunlem3

	Ref	Expression
Hypotheses	voliunlem.3	$⊢ φ \to F : ℕ ⟶ dom vol$
	voliunlem.5	$⊢ φ \to \underset{i \in ℕ}{Disj} F (i)$
	voliunlem.6	$⊢ H = (n \in ℕ ⟼ {vol}^{*} (x \cap F (n)))$
	voliunlem3.1	$⊢ S = seq 1 (+ G)$
	voliunlem3.2	$⊢ G = (n \in ℕ ⟼ vol (F (n)))$
	voliunlem3.4	$⊢ φ \to \forall i \in ℕ vol (F (i)) \in ℝ$
Assertion	voliunlem3	$⊢ φ \to vol (⋃ ran F) = sup (ran S ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		voliunlem.3	$⊢ φ \to F : ℕ ⟶ dom vol$
2		voliunlem.5	$⊢ φ \to \underset{i \in ℕ}{Disj} F (i)$
3		voliunlem.6	$⊢ H = (n \in ℕ ⟼ {vol}^{*} (x \cap F (n)))$
4		voliunlem3.1	$⊢ S = seq 1 (+ G)$
5		voliunlem3.2	$⊢ G = (n \in ℕ ⟼ vol (F (n)))$
6		voliunlem3.4	$⊢ φ \to \forall i \in ℕ vol (F (i)) \in ℝ$
7	1 2 3	voliunlem2	$⊢ φ \to ⋃ ran F \in dom vol$
8		mblvol	$⊢ ⋃ ran F \in dom vol \to vol (⋃ ran F) = {vol}^{*} (⋃ ran F)$
9	7 8	syl	$⊢ φ \to vol (⋃ ran F) = {vol}^{*} (⋃ ran F)$
10	1	frnd	$⊢ φ \to ran F \subseteq dom vol$
11		mblss	$⊢ x \in dom vol \to x \subseteq ℝ$
12		reex	$⊢ ℝ \in V$
13	12	elpw2	$⊢ x \in 𝒫 ℝ \leftrightarrow x \subseteq ℝ$
14	11 13	sylibr	$⊢ x \in dom vol \to x \in 𝒫 ℝ$
15	14	ssriv	$⊢ dom vol \subseteq 𝒫 ℝ$
16	10 15	sstrdi	$⊢ φ \to ran F \subseteq 𝒫 ℝ$
17		sspwuni	$⊢ ran F \subseteq 𝒫 ℝ \leftrightarrow ⋃ ran F \subseteq ℝ$
18	16 17	sylib	$⊢ φ \to ⋃ ran F \subseteq ℝ$
19		ovolcl	$⊢ ⋃ ran F \subseteq ℝ \to {vol}^{} (⋃ ran F) \in ℝ^{}$
20	18 19	syl	$⊢ φ \to {vol}^{} (⋃ ran F) \in ℝ^{}$
21		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
22		1zzd	$⊢ φ \to 1 \in ℤ$
23		2fveq3	$⊢ n = k \to vol (F (n)) = vol (F (k))$
24		fvex	$⊢ vol (F (k)) \in V$
25	23 5 24	fvmpt	$⊢ k \in ℕ \to G (k) = vol (F (k))$
26	25	adantl	$⊢ (φ \land k \in ℕ) \to G (k) = vol (F (k))$
27		2fveq3	$⊢ i = k \to vol (F (i)) = vol (F (k))$
28	27	eleq1d	$⊢ i = k \to (vol (F (i)) \in ℝ \leftrightarrow vol (F (k)) \in ℝ)$
29	28	rspccva	$⊢ (\forall i \in ℕ vol (F (i)) \in ℝ \land k \in ℕ) \to vol (F (k)) \in ℝ$
30	6 29	sylan	$⊢ (φ \land k \in ℕ) \to vol (F (k)) \in ℝ$
31	26 30	eqeltrd	$⊢ (φ \land k \in ℕ) \to G (k) \in ℝ$
32	21 22 31	serfre	$⊢ φ \to seq 1 (+ G) : ℕ ⟶ ℝ$
33	4	feq1i	$⊢ S : ℕ ⟶ ℝ \leftrightarrow seq 1 (+ G) : ℕ ⟶ ℝ$
34	32 33	sylibr	$⊢ φ \to S : ℕ ⟶ ℝ$
35	34	frnd	$⊢ φ \to ran S \subseteq ℝ$
36		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
37	35 36	sstrdi	$⊢ φ \to ran S \subseteq ℝ^{*}$
38		supxrcl	$⊢ ran S \subseteq ℝ^{} \to sup (ran S ℝ^{} <) \in ℝ^{*}$
39	37 38	syl	$⊢ φ \to sup (ran S ℝ^{} <) \in ℝ^{}$
40		eqid	$⊢ seq 1 (+ (n \in ℕ ⟼ {vol}^{} (F (n)))) = seq 1 (+ (n \in ℕ ⟼ {vol}^{} (F (n))))$
41		eqid	$⊢ (n \in ℕ ⟼ {vol}^{} (F (n))) = (n \in ℕ ⟼ {vol}^{} (F (n)))$
42	1	ffvelrnda	$⊢ (φ \land n \in ℕ) \to F (n) \in dom vol$
43		mblss	$⊢ F (n) \in dom vol \to F (n) \subseteq ℝ$
44	42 43	syl	$⊢ (φ \land n \in ℕ) \to F (n) \subseteq ℝ$
45		mblvol	$⊢ F (n) \in dom vol \to vol (F (n)) = {vol}^{*} (F (n))$
46	42 45	syl	$⊢ (φ \land n \in ℕ) \to vol (F (n)) = {vol}^{*} (F (n))$
47		2fveq3	$⊢ i = n \to vol (F (i)) = vol (F (n))$
48	47	eleq1d	$⊢ i = n \to (vol (F (i)) \in ℝ \leftrightarrow vol (F (n)) \in ℝ)$
49	48	rspccva	$⊢ (\forall i \in ℕ vol (F (i)) \in ℝ \land n \in ℕ) \to vol (F (n)) \in ℝ$
50	6 49	sylan	$⊢ (φ \land n \in ℕ) \to vol (F (n)) \in ℝ$
51	46 50	eqeltrrd	$⊢ (φ \land n \in ℕ) \to {vol}^{*} (F (n)) \in ℝ$
52	40 41 44 51	ovoliun	$⊢ φ \to {vol}^{} (⋃_{n \in ℕ} F (n)) \leq sup (ran seq 1 (+ (n \in ℕ ⟼ {vol}^{} (F (n)))) ℝ^{*} <)$
53	1	ffnd	$⊢ φ \to F Fn ℕ$
54		fniunfv	$⊢ F Fn ℕ \to ⋃_{n \in ℕ} F (n) = ⋃ ran F$
55	53 54	syl	$⊢ φ \to ⋃_{n \in ℕ} F (n) = ⋃ ran F$
56	55	fveq2d	$⊢ φ \to {vol}^{} (⋃_{n \in ℕ} F (n)) = {vol}^{} (⋃ ran F)$
57	46	mpteq2dva	$⊢ φ \to (n \in ℕ ⟼ vol (F (n))) = (n \in ℕ ⟼ {vol}^{*} (F (n)))$
58	5 57	syl5eq	$⊢ φ \to G = (n \in ℕ ⟼ {vol}^{*} (F (n)))$
59	58	seqeq3d	$⊢ φ \to seq 1 (+ G) = seq 1 (+ (n \in ℕ ⟼ {vol}^{*} (F (n))))$
60	4 59	syl5req	$⊢ φ \to seq 1 (+ (n \in ℕ ⟼ {vol}^{*} (F (n)))) = S$
61	60	rneqd	$⊢ φ \to ran seq 1 (+ (n \in ℕ ⟼ {vol}^{*} (F (n)))) = ran S$
62	61	supeq1d	$⊢ φ \to sup (ran seq 1 (+ (n \in ℕ ⟼ {vol}^{} (F (n)))) ℝ^{} <) = sup (ran S ℝ^{*} <)$
63	52 56 62	3brtr3d	$⊢ φ \to {vol}^{} (⋃ ran F) \leq sup (ran S ℝ^{} <)$
64		ovolge0	$⊢ ⋃ ran F \subseteq ℝ \to 0 \leq {vol}^{*} (⋃ ran F)$
65	18 64	syl	$⊢ φ \to 0 \leq {vol}^{*} (⋃ ran F)$
66		mnflt0	$⊢ −∞ < 0$
67		mnfxr	$⊢ −∞ \in ℝ^{*}$
68		0xr	$⊢ 0 \in ℝ^{*}$
69		xrltletr	$⊢ (−∞ \in ℝ^{} \land 0 \in ℝ^{} \land {vol}^{} (⋃ ran F) \in ℝ^{}) \to ((−∞ < 0 \land 0 \leq {vol}^{} (⋃ ran F)) \to −∞ < {vol}^{} (⋃ ran F))$
70	67 68 69	mp3an12	$⊢ {vol}^{} (⋃ ran F) \in ℝ^{} \to ((−∞ < 0 \land 0 \leq {vol}^{} (⋃ ran F)) \to −∞ < {vol}^{} (⋃ ran F))$
71	66 70	mpani	$⊢ {vol}^{} (⋃ ran F) \in ℝ^{} \to (0 \leq {vol}^{} (⋃ ran F) \to −∞ < {vol}^{} (⋃ ran F))$
72	20 65 71	sylc	$⊢ φ \to −∞ < {vol}^{*} (⋃ ran F)$
73		xrrebnd	$⊢ {vol}^{} (⋃ ran F) \in ℝ^{} \to ({vol}^{} (⋃ ran F) \in ℝ \leftrightarrow (−∞ < {vol}^{} (⋃ ran F) \land {vol}^{*} (⋃ ran F) < +∞))$
74	20 73	syl	$⊢ φ \to ({vol}^{} (⋃ ran F) \in ℝ \leftrightarrow (−∞ < {vol}^{} (⋃ ran F) \land {vol}^{*} (⋃ ran F) < +∞))$
75	12	elpw2	$⊢ ⋃ ran F \in 𝒫 ℝ \leftrightarrow ⋃ ran F \subseteq ℝ$
76	18 75	sylibr	$⊢ φ \to ⋃ ran F \in 𝒫 ℝ$
77		simpl	$⊢ (x = ⋃ ran F \land φ) \to x = ⋃ ran F$
78	77	sseq1d	$⊢ (x = ⋃ ran F \land φ) \to (x \subseteq ℝ \leftrightarrow ⋃ ran F \subseteq ℝ)$
79	77	fveq2d	$⊢ (x = ⋃ ran F \land φ) \to {vol}^{} (x) = {vol}^{} (⋃ ran F)$
80	79	eleq1d	$⊢ (x = ⋃ ran F \land φ) \to ({vol}^{} (x) \in ℝ \leftrightarrow {vol}^{} (⋃ ran F) \in ℝ)$
81		simpll	$⊢ ((x = ⋃ ran F \land φ) \land n \in ℕ) \to x = ⋃ ran F$
82	81	ineq1d	$⊢ ((x = ⋃ ran F \land φ) \land n \in ℕ) \to x \cap F (n) = ⋃ ran F \cap F (n)$
83		fnfvelrn	$⊢ (F Fn ℕ \land n \in ℕ) \to F (n) \in ran F$
84	53 83	sylan	$⊢ (φ \land n \in ℕ) \to F (n) \in ran F$
85		elssuni	$⊢ F (n) \in ran F \to F (n) \subseteq ⋃ ran F$
86	84 85	syl	$⊢ (φ \land n \in ℕ) \to F (n) \subseteq ⋃ ran F$
87	86	adantll	$⊢ ((x = ⋃ ran F \land φ) \land n \in ℕ) \to F (n) \subseteq ⋃ ran F$
88		sseqin2	$⊢ F (n) \subseteq ⋃ ran F \leftrightarrow ⋃ ran F \cap F (n) = F (n)$
89	87 88	sylib	$⊢ ((x = ⋃ ran F \land φ) \land n \in ℕ) \to ⋃ ran F \cap F (n) = F (n)$
90	82 89	eqtrd	$⊢ ((x = ⋃ ran F \land φ) \land n \in ℕ) \to x \cap F (n) = F (n)$
91	90	fveq2d	$⊢ ((x = ⋃ ran F \land φ) \land n \in ℕ) \to {vol}^{} (x \cap F (n)) = {vol}^{} (F (n))$
92	46	adantll	$⊢ ((x = ⋃ ran F \land φ) \land n \in ℕ) \to vol (F (n)) = {vol}^{*} (F (n))$
93	91 92	eqtr4d	$⊢ ((x = ⋃ ran F \land φ) \land n \in ℕ) \to {vol}^{*} (x \cap F (n)) = vol (F (n))$
94	93	mpteq2dva	$⊢ (x = ⋃ ran F \land φ) \to (n \in ℕ ⟼ {vol}^{*} (x \cap F (n))) = (n \in ℕ ⟼ vol (F (n)))$
95	94	adantrr	$⊢ (x = ⋃ ran F \land (φ \land k \in ℕ)) \to (n \in ℕ ⟼ {vol}^{*} (x \cap F (n))) = (n \in ℕ ⟼ vol (F (n)))$
96	95 3 5	3eqtr4g	$⊢ (x = ⋃ ran F \land (φ \land k \in ℕ)) \to H = G$
97	96	seqeq3d	$⊢ (x = ⋃ ran F \land (φ \land k \in ℕ)) \to seq 1 (+ H) = seq 1 (+ G)$
98	97 4	eqtr4di	$⊢ (x = ⋃ ran F \land (φ \land k \in ℕ)) \to seq 1 (+ H) = S$
99	98	fveq1d	$⊢ (x = ⋃ ran F \land (φ \land k \in ℕ)) \to seq 1 (+ H) (k) = S (k)$
100		difeq1	$⊢ x = ⋃ ran F \to x ∖ ⋃ ran F = ⋃ ran F ∖ ⋃ ran F$
101		difid	$⊢ ⋃ ran F ∖ ⋃ ran F = \emptyset$
102	100 101	eqtrdi	$⊢ x = ⋃ ran F \to x ∖ ⋃ ran F = \emptyset$
103	102	fveq2d	$⊢ x = ⋃ ran F \to {vol}^{} (x ∖ ⋃ ran F) = {vol}^{} (\emptyset)$
104		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
105	103 104	eqtrdi	$⊢ x = ⋃ ran F \to {vol}^{*} (x ∖ ⋃ ran F) = 0$
106	105	adantr	$⊢ (x = ⋃ ran F \land (φ \land k \in ℕ)) \to {vol}^{*} (x ∖ ⋃ ran F) = 0$
107	99 106	oveq12d	$⊢ (x = ⋃ ran F \land (φ \land k \in ℕ)) \to seq 1 (+ H) (k) + {vol}^{*} (x ∖ ⋃ ran F) = S (k) + 0$
108	34	ffvelrnda	$⊢ (φ \land k \in ℕ) \to S (k) \in ℝ$
109	108	adantl	$⊢ (x = ⋃ ran F \land (φ \land k \in ℕ)) \to S (k) \in ℝ$
110	109	recnd	$⊢ (x = ⋃ ran F \land (φ \land k \in ℕ)) \to S (k) \in ℂ$
111	110	addid1d	$⊢ (x = ⋃ ran F \land (φ \land k \in ℕ)) \to S (k) + 0 = S (k)$
112	107 111	eqtrd	$⊢ (x = ⋃ ran F \land (φ \land k \in ℕ)) \to seq 1 (+ H) (k) + {vol}^{*} (x ∖ ⋃ ran F) = S (k)$
113		fveq2	$⊢ x = ⋃ ran F \to {vol}^{} (x) = {vol}^{} (⋃ ran F)$
114	113	adantr	$⊢ (x = ⋃ ran F \land (φ \land k \in ℕ)) \to {vol}^{} (x) = {vol}^{} (⋃ ran F)$
115	112 114	breq12d	$⊢ (x = ⋃ ran F \land (φ \land k \in ℕ)) \to (seq 1 (+ H) (k) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{} (x) \leftrightarrow S (k) \leq {vol}^{*} (⋃ ran F))$
116	115	expr	$⊢ (x = ⋃ ran F \land φ) \to (k \in ℕ \to (seq 1 (+ H) (k) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{} (x) \leftrightarrow S (k) \leq {vol}^{*} (⋃ ran F)))$
117	116	pm5.74d	$⊢ (x = ⋃ ran F \land φ) \to ((k \in ℕ \to seq 1 (+ H) (k) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{} (x)) \leftrightarrow (k \in ℕ \to S (k) \leq {vol}^{*} (⋃ ran F)))$
118	80 117	imbi12d	$⊢ (x = ⋃ ran F \land φ) \to (({vol}^{} (x) \in ℝ \to (k \in ℕ \to seq 1 (+ H) (k) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{} (x))) \leftrightarrow ({vol}^{} (⋃ ran F) \in ℝ \to (k \in ℕ \to S (k) \leq {vol}^{*} (⋃ ran F))))$
119	78 118	imbi12d	$⊢ (x = ⋃ ran F \land φ) \to ((x \subseteq ℝ \to ({vol}^{} (x) \in ℝ \to (k \in ℕ \to seq 1 (+ H) (k) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{} (x)))) \leftrightarrow (⋃ ran F \subseteq ℝ \to ({vol}^{} (⋃ ran F) \in ℝ \to (k \in ℕ \to S (k) \leq {vol}^{*} (⋃ ran F)))))$
120	119	pm5.74da	$⊢ x = ⋃ ran F \to ((φ \to (x \subseteq ℝ \to ({vol}^{} (x) \in ℝ \to (k \in ℕ \to seq 1 (+ H) (k) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{} (x))))) \leftrightarrow (φ \to (⋃ ran F \subseteq ℝ \to ({vol}^{} (⋃ ran F) \in ℝ \to (k \in ℕ \to S (k) \leq {vol}^{*} (⋃ ran F))))))$
121	1	3ad2ant1	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to F : ℕ ⟶ dom vol$
122	2	3ad2ant1	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to \underset{i \in ℕ}{Disj} F (i)$
123		simp2	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to x \subseteq ℝ$
124		simp3	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x) \in ℝ$
125	121 122 3 123 124	voliunlem1	$⊢ ((φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \land k \in ℕ) \to seq 1 (+ H) (k) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{*} (x)$
126	125	3exp1	$⊢ φ \to (x \subseteq ℝ \to ({vol}^{} (x) \in ℝ \to (k \in ℕ \to seq 1 (+ H) (k) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{*} (x))))$
127	120 126	vtoclg	$⊢ ⋃ ran F \in 𝒫 ℝ \to (φ \to (⋃ ran F \subseteq ℝ \to ({vol}^{} (⋃ ran F) \in ℝ \to (k \in ℕ \to S (k) \leq {vol}^{} (⋃ ran F)))))$
128	76 127	mpcom	$⊢ φ \to (⋃ ran F \subseteq ℝ \to ({vol}^{} (⋃ ran F) \in ℝ \to (k \in ℕ \to S (k) \leq {vol}^{} (⋃ ran F))))$
129	18 128	mpd	$⊢ φ \to ({vol}^{} (⋃ ran F) \in ℝ \to (k \in ℕ \to S (k) \leq {vol}^{} (⋃ ran F)))$
130	74 129	sylbird	$⊢ φ \to ((−∞ < {vol}^{} (⋃ ran F) \land {vol}^{} (⋃ ran F) < +∞) \to (k \in ℕ \to S (k) \leq {vol}^{*} (⋃ ran F)))$
131	72 130	mpand	$⊢ φ \to ({vol}^{} (⋃ ran F) < +∞ \to (k \in ℕ \to S (k) \leq {vol}^{} (⋃ ran F)))$
132		nltpnft	$⊢ {vol}^{} (⋃ ran F) \in ℝ^{} \to ({vol}^{} (⋃ ran F) = +∞ \leftrightarrow \neg {vol}^{} (⋃ ran F) < +∞)$
133	20 132	syl	$⊢ φ \to ({vol}^{} (⋃ ran F) = +∞ \leftrightarrow \neg {vol}^{} (⋃ ran F) < +∞)$
134		rexr	$⊢ S (k) \in ℝ \to S (k) \in ℝ^{*}$
135		pnfge	$⊢ S (k) \in ℝ^{*} \to S (k) \leq +∞$
136	108 134 135	3syl	$⊢ (φ \land k \in ℕ) \to S (k) \leq +∞$
137	136	ex	$⊢ φ \to (k \in ℕ \to S (k) \leq +∞)$
138		breq2	$⊢ {vol}^{} (⋃ ran F) = +∞ \to (S (k) \leq {vol}^{} (⋃ ran F) \leftrightarrow S (k) \leq +∞)$
139	138	imbi2d	$⊢ {vol}^{} (⋃ ran F) = +∞ \to ((k \in ℕ \to S (k) \leq {vol}^{} (⋃ ran F)) \leftrightarrow (k \in ℕ \to S (k) \leq +∞))$
140	137 139	syl5ibrcom	$⊢ φ \to ({vol}^{} (⋃ ran F) = +∞ \to (k \in ℕ \to S (k) \leq {vol}^{} (⋃ ran F)))$
141	133 140	sylbird	$⊢ φ \to (\neg {vol}^{} (⋃ ran F) < +∞ \to (k \in ℕ \to S (k) \leq {vol}^{} (⋃ ran F)))$
142	131 141	pm2.61d	$⊢ φ \to (k \in ℕ \to S (k) \leq {vol}^{*} (⋃ ran F))$
143	142	ralrimiv	$⊢ φ \to \forall k \in ℕ S (k) \leq {vol}^{*} (⋃ ran F)$
144	34	ffnd	$⊢ φ \to S Fn ℕ$
145		breq1	$⊢ z = S (k) \to (z \leq {vol}^{} (⋃ ran F) \leftrightarrow S (k) \leq {vol}^{} (⋃ ran F))$
146	145	ralrn	$⊢ S Fn ℕ \to (\forall z \in ran S z \leq {vol}^{} (⋃ ran F) \leftrightarrow \forall k \in ℕ S (k) \leq {vol}^{} (⋃ ran F))$
147	144 146	syl	$⊢ φ \to (\forall z \in ran S z \leq {vol}^{} (⋃ ran F) \leftrightarrow \forall k \in ℕ S (k) \leq {vol}^{} (⋃ ran F))$
148	143 147	mpbird	$⊢ φ \to \forall z \in ran S z \leq {vol}^{*} (⋃ ran F)$
149		supxrleub	$⊢ (ran S \subseteq ℝ^{} \land {vol}^{} (⋃ ran F) \in ℝ^{}) \to (sup (ran S ℝ^{} <) \leq {vol}^{} (⋃ ran F) \leftrightarrow \forall z \in ran S z \leq {vol}^{} (⋃ ran F))$
150	37 20 149	syl2anc	$⊢ φ \to (sup (ran S ℝ^{} <) \leq {vol}^{} (⋃ ran F) \leftrightarrow \forall z \in ran S z \leq {vol}^{*} (⋃ ran F))$
151	148 150	mpbird	$⊢ φ \to sup (ran S ℝ^{} <) \leq {vol}^{} (⋃ ran F)$
152	20 39 63 151	xrletrid	$⊢ φ \to {vol}^{} (⋃ ran F) = sup (ran S ℝ^{} <)$
153	9 152	eqtrd	$⊢ φ \to vol (⋃ ran F) = sup (ran S ℝ^{*} <)$

Metamath Proof Explorer

Theorem voliunlem3

Proof