voliunlem2

	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)))$
Assertion	voliunlem2	$⊢ φ \to ⋃ ran F \in dom vol$

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	1	frnd	$⊢ φ \to ran F \subseteq dom vol$
5		mblss	$⊢ x \in dom vol \to x \subseteq ℝ$
6		velpw	$⊢ x \in 𝒫 ℝ \leftrightarrow x \subseteq ℝ$
7	5 6	sylibr	$⊢ x \in dom vol \to x \in 𝒫 ℝ$
8	7	ssriv	$⊢ dom vol \subseteq 𝒫 ℝ$
9	4 8	sstrdi	$⊢ φ \to ran F \subseteq 𝒫 ℝ$
10		sspwuni	$⊢ ran F \subseteq 𝒫 ℝ \leftrightarrow ⋃ ran F \subseteq ℝ$
11	9 10	sylib	$⊢ φ \to ⋃ ran F \subseteq ℝ$
12		elpwi	$⊢ x \in 𝒫 ℝ \to x \subseteq ℝ$
13		inundif	$⊢ (x \cap ⋃ ran F) \cup (x ∖ ⋃ ran F) = x$
14	13	fveq2i	$⊢ {vol}^{} ((x \cap ⋃ ran F) \cup (x ∖ ⋃ ran F)) = {vol}^{} (x)$
15		inss1	$⊢ x \cap ⋃ ran F \subseteq x$
16		simp2	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to x \subseteq ℝ$
17	15 16	sstrid	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to x \cap ⋃ ran F \subseteq ℝ$
18		ovolsscl	$⊢ (x \cap ⋃ ran F \subseteq x \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap ⋃ ran F) \in ℝ$
19	15 18	mp3an1	$⊢ (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap ⋃ ran F) \in ℝ$
20	19	3adant1	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap ⋃ ran F) \in ℝ$
21		difss	$⊢ x ∖ ⋃ ran F \subseteq x$
22	21 16	sstrid	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to x ∖ ⋃ ran F \subseteq ℝ$
23		ovolsscl	$⊢ (x ∖ ⋃ ran F \subseteq x \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x ∖ ⋃ ran F) \in ℝ$
24	21 23	mp3an1	$⊢ (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x ∖ ⋃ ran F) \in ℝ$
25	24	3adant1	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x ∖ ⋃ ran F) \in ℝ$
26		ovolun	$⊢ ((x \cap ⋃ ran F \subseteq ℝ \land {vol}^{} (x \cap ⋃ ran F) \in ℝ) \land (x ∖ ⋃ ran F \subseteq ℝ \land {vol}^{} (x ∖ ⋃ ran F) \in ℝ)) \to {vol}^{} ((x \cap ⋃ ran F) \cup (x ∖ ⋃ ran F)) \leq {vol}^{} (x \cap ⋃ ran F) + {vol}^{*} (x ∖ ⋃ ran F)$
27	17 20 22 25 26	syl22anc	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} ((x \cap ⋃ ran F) \cup (x ∖ ⋃ ran F)) \leq {vol}^{} (x \cap ⋃ ran F) + {vol}^{} (x ∖ ⋃ ran F)$
28	14 27	eqbrtrrid	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x) \leq {vol}^{} (x \cap ⋃ ran F) + {vol}^{} (x ∖ ⋃ ran F)$
29	20	rexrd	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap ⋃ ran F) \in ℝ^{*}$
30		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
31		1zzd	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to 1 \in ℤ$
32		fveq2	$⊢ n = k \to F (n) = F (k)$
33	32	ineq2d	$⊢ n = k \to x \cap F (n) = x \cap F (k)$
34	33	fveq2d	$⊢ n = k \to {vol}^{} (x \cap F (n)) = {vol}^{} (x \cap F (k))$
35		fvex	$⊢ {vol}^{*} (x \cap F (k)) \in V$
36	34 3 35	fvmpt	$⊢ k \in ℕ \to H (k) = {vol}^{*} (x \cap F (k))$
37	36	adantl	$⊢ ((φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \land k \in ℕ) \to H (k) = {vol}^{} (x \cap F (k))$
38		inss1	$⊢ x \cap F (k) \subseteq x$
39		ovolsscl	$⊢ (x \cap F (k) \subseteq x \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap F (k)) \in ℝ$
40	38 39	mp3an1	$⊢ (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap F (k)) \in ℝ$
41	40	3adant1	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap F (k)) \in ℝ$
42	41	adantr	$⊢ ((φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \land k \in ℕ) \to {vol}^{} (x \cap F (k)) \in ℝ$
43	37 42	eqeltrd	$⊢ ((φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \land k \in ℕ) \to H (k) \in ℝ$
44	30 31 43	serfre	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to seq 1 (+ H) : ℕ ⟶ ℝ$
45	44	frnd	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to ran seq 1 (+ H) \subseteq ℝ$
46		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
47	45 46	sstrdi	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to ran seq 1 (+ H) \subseteq ℝ^{}$
48		supxrcl	$⊢ ran seq 1 (+ H) \subseteq ℝ^{} \to sup (ran seq 1 (+ H) ℝ^{} <) \in ℝ^{*}$
49	47 48	syl	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to sup (ran seq 1 (+ H) ℝ^{} <) \in ℝ^{*}$
50		simp3	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x) \in ℝ$
51	50 25	resubcld	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x) - {vol}^{*} (x ∖ ⋃ ran F) \in ℝ$
52	51	rexrd	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x) - {vol}^{} (x ∖ ⋃ ran F) \in ℝ^{}$
53		iunin2	$⊢ ⋃_{n \in ℕ} (x \cap F (n)) = x \cap ⋃_{n \in ℕ} F (n)$
54		ffn	$⊢ F : ℕ ⟶ dom vol \to F Fn ℕ$
55		fniunfv	$⊢ F Fn ℕ \to ⋃_{n \in ℕ} F (n) = ⋃ ran F$
56	1 54 55	3syl	$⊢ φ \to ⋃_{n \in ℕ} F (n) = ⋃ ran F$
57	56	3ad2ant1	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to ⋃_{n \in ℕ} F (n) = ⋃ ran F$
58	57	ineq2d	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to x \cap ⋃_{n \in ℕ} F (n) = x \cap ⋃ ran F$
59	53 58	syl5eq	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to ⋃_{n \in ℕ} (x \cap F (n)) = x \cap ⋃ ran F$
60	59	fveq2d	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (⋃_{n \in ℕ} (x \cap F (n))) = {vol}^{*} (x \cap ⋃ ran F)$
61		eqid	$⊢ seq 1 (+ H) = seq 1 (+ H)$
62		inss1	$⊢ x \cap F (n) \subseteq x$
63	62 16	sstrid	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to x \cap F (n) \subseteq ℝ$
64	63	adantr	$⊢ ((φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \land n \in ℕ) \to x \cap F (n) \subseteq ℝ$
65		ovolsscl	$⊢ (x \cap F (n) \subseteq x \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap F (n)) \in ℝ$
66	62 65	mp3an1	$⊢ (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap F (n)) \in ℝ$
67	66	3adant1	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap F (n)) \in ℝ$
68	67	adantr	$⊢ ((φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \land n \in ℕ) \to {vol}^{} (x \cap F (n)) \in ℝ$
69	61 3 64 68	ovoliun	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (⋃_{n \in ℕ} (x \cap F (n))) \leq sup (ran seq 1 (+ H) ℝ^{*} <)$
70	60 69	eqbrtrrd	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap ⋃ ran F) \leq sup (ran seq 1 (+ H) ℝ^{*} <)$
71	1	3ad2ant1	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to F : ℕ ⟶ dom vol$
72	2	3ad2ant1	$⊢ (φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \to \underset{i \in ℕ}{Disj} F (i)$
73	71 72 3 16 50	voliunlem1	$⊢ ((φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \land k \in ℕ) \to seq 1 (+ H) (k) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{*} (x)$
74	44	ffvelrnda	$⊢ ((φ \land x \subseteq ℝ \land {vol}^{*} (x) \in ℝ) \land k \in ℕ) \to seq 1 (+ H) (k) \in ℝ$
75	25	adantr	$⊢ ((φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \land k \in ℕ) \to {vol}^{} (x ∖ ⋃ ran F) \in ℝ$
76		simpl3	$⊢ ((φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \land k \in ℕ) \to {vol}^{} (x) \in ℝ$
77		leaddsub	$⊢ (seq 1 (+ H) (k) \in ℝ \land {vol}^{} (x ∖ ⋃ ran F) \in ℝ \land {vol}^{} (x) \in ℝ) \to (seq 1 (+ H) (k) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{} (x) \leftrightarrow seq 1 (+ H) (k) \leq {vol}^{} (x) - {vol}^{} (x ∖ ⋃ ran F))$
78	74 75 76 77	syl3anc	$⊢ ((φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \land k \in ℕ) \to (seq 1 (+ H) (k) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{} (x) \leftrightarrow seq 1 (+ H) (k) \leq {vol}^{} (x) - {vol}^{*} (x ∖ ⋃ ran F))$
79	73 78	mpbid	$⊢ ((φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \land k \in ℕ) \to seq 1 (+ H) (k) \leq {vol}^{} (x) - {vol}^{*} (x ∖ ⋃ ran F)$
80	79	ralrimiva	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to \forall k \in ℕ seq 1 (+ H) (k) \leq {vol}^{} (x) - {vol}^{*} (x ∖ ⋃ ran F)$
81		ffn	$⊢ seq 1 (+ H) : ℕ ⟶ ℝ \to seq 1 (+ H) Fn ℕ$
82		breq1	$⊢ z = seq 1 (+ H) (k) \to (z \leq {vol}^{} (x) - {vol}^{} (x ∖ ⋃ ran F) \leftrightarrow seq 1 (+ H) (k) \leq {vol}^{} (x) - {vol}^{} (x ∖ ⋃ ran F))$
83	82	ralrn	$⊢ seq 1 (+ H) Fn ℕ \to (\forall z \in ran seq 1 (+ H) z \leq {vol}^{} (x) - {vol}^{} (x ∖ ⋃ ran F) \leftrightarrow \forall k \in ℕ seq 1 (+ H) (k) \leq {vol}^{} (x) - {vol}^{} (x ∖ ⋃ ran F))$
84	44 81 83	3syl	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to (\forall z \in ran seq 1 (+ H) z \leq {vol}^{} (x) - {vol}^{} (x ∖ ⋃ ran F) \leftrightarrow \forall k \in ℕ seq 1 (+ H) (k) \leq {vol}^{} (x) - {vol}^{*} (x ∖ ⋃ ran F))$
85	80 84	mpbird	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to \forall z \in ran seq 1 (+ H) z \leq {vol}^{} (x) - {vol}^{*} (x ∖ ⋃ ran F)$
86		supxrleub	$⊢ (ran seq 1 (+ H) \subseteq ℝ^{} \land {vol}^{} (x) - {vol}^{} (x ∖ ⋃ ran F) \in ℝ^{}) \to (sup (ran seq 1 (+ H) ℝ^{} <) \leq {vol}^{} (x) - {vol}^{} (x ∖ ⋃ ran F) \leftrightarrow \forall z \in ran seq 1 (+ H) z \leq {vol}^{} (x) - {vol}^{*} (x ∖ ⋃ ran F))$
87	47 52 86	syl2anc	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to (sup (ran seq 1 (+ H) ℝ^{} <) \leq {vol}^{} (x) - {vol}^{} (x ∖ ⋃ ran F) \leftrightarrow \forall z \in ran seq 1 (+ H) z \leq {vol}^{} (x) - {vol}^{} (x ∖ ⋃ ran F))$
88	85 87	mpbird	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to sup (ran seq 1 (+ H) ℝ^{} <) \leq {vol}^{} (x) - {vol}^{} (x ∖ ⋃ ran F)$
89	29 49 52 70 88	xrletrd	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap ⋃ ran F) \leq {vol}^{} (x) - {vol}^{} (x ∖ ⋃ ran F)$
90		leaddsub	$⊢ ({vol}^{} (x \cap ⋃ ran F) \in ℝ \land {vol}^{} (x ∖ ⋃ ran F) \in ℝ \land {vol}^{} (x) \in ℝ) \to ({vol}^{} (x \cap ⋃ ran F) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{} (x) \leftrightarrow {vol}^{} (x \cap ⋃ ran F) \leq {vol}^{} (x) - {vol}^{*} (x ∖ ⋃ ran F))$
91	20 25 50 90	syl3anc	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to ({vol}^{} (x \cap ⋃ ran F) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{} (x) \leftrightarrow {vol}^{} (x \cap ⋃ ran F) \leq {vol}^{} (x) - {vol}^{*} (x ∖ ⋃ ran F))$
92	89 91	mpbird	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap ⋃ ran F) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{} (x)$
93	20 25	readdcld	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap ⋃ ran F) + {vol}^{*} (x ∖ ⋃ ran F) \in ℝ$
94	50 93	letri3d	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to ({vol}^{} (x) = {vol}^{} (x \cap ⋃ ran F) + {vol}^{} (x ∖ ⋃ ran F) \leftrightarrow ({vol}^{} (x) \leq {vol}^{} (x \cap ⋃ ran F) + {vol}^{} (x ∖ ⋃ ran F) \land {vol}^{} (x \cap ⋃ ran F) + {vol}^{} (x ∖ ⋃ ran F) \leq {vol}^{} (x)))$
95	28 92 94	mpbir2and	$⊢ (φ \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x) = {vol}^{} (x \cap ⋃ ran F) + {vol}^{} (x ∖ ⋃ ran F)$
96	95	3expia	$⊢ (φ \land x \subseteq ℝ) \to ({vol}^{} (x) \in ℝ \to {vol}^{} (x) = {vol}^{} (x \cap ⋃ ran F) + {vol}^{} (x ∖ ⋃ ran F))$
97	12 96	sylan2	$⊢ (φ \land x \in 𝒫 ℝ) \to ({vol}^{} (x) \in ℝ \to {vol}^{} (x) = {vol}^{} (x \cap ⋃ ran F) + {vol}^{} (x ∖ ⋃ ran F))$
98	97	ralrimiva	$⊢ φ \to \forall x \in 𝒫 ℝ ({vol}^{} (x) \in ℝ \to {vol}^{} (x) = {vol}^{} (x \cap ⋃ ran F) + {vol}^{} (x ∖ ⋃ ran F))$
99		ismbl	$⊢ ⋃ ran F \in dom vol \leftrightarrow (⋃ ran F \subseteq ℝ \land \forall x \in 𝒫 ℝ ({vol}^{} (x) \in ℝ \to {vol}^{} (x) = {vol}^{} (x \cap ⋃ ran F) + {vol}^{} (x ∖ ⋃ ran F)))$
100	11 98 99	sylanbrc	$⊢ φ \to ⋃ ran F \in dom vol$

Metamath Proof Explorer

Theorem voliunlem2

Proof