ovoliunlem2

	Ref	Expression
Hypotheses	ovoliun.t	$⊢ T = seq 1 (+ G)$
	ovoliun.g	$⊢ G = (n \in ℕ ⟼ {vol}^{*} (A))$
	ovoliun.a	$⊢ (φ \land n \in ℕ) \to A \subseteq ℝ$
	ovoliun.v	$⊢ (φ \land n \in ℕ) \to {vol}^{*} (A) \in ℝ$
	ovoliun.r	$⊢ φ \to sup (ran T ℝ^{*} <) \in ℝ$
	ovoliun.b	$⊢ φ \to B \in ℝ^{+}$
	ovoliun.s	$⊢ S = seq 1 (+ ((abs \circ -) \circ F (n)))$
	ovoliun.u	$⊢ U = seq 1 (+ ((abs \circ -) \circ H))$
	ovoliun.h	$⊢ H = (k \in ℕ ⟼ F (1^{st} (J (k))) (2^{nd} (J (k))))$
	ovoliun.j	$⊢ φ \to J : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ$
	ovoliun.f	$⊢ φ \to F : ℕ ⟶ {(\leq \cap ℝ^{2})}^{ℕ}$
	ovoliun.x1	$⊢ (φ \land n \in ℕ) \to A \subseteq ⋃ ran ((.) \circ F (n))$
	ovoliun.x2	$⊢ (φ \land n \in ℕ) \to sup (ran S ℝ^{} <) \leq {vol}^{} (A) + (\frac{B}{2^{n}})$
Assertion	ovoliunlem2	$⊢ φ \to {vol}^{} (⋃_{n \in ℕ} A) \leq sup (ran T ℝ^{} <) + B$

Proof

Step	Hyp	Ref	Expression
1		ovoliun.t	$⊢ T = seq 1 (+ G)$
2		ovoliun.g	$⊢ G = (n \in ℕ ⟼ {vol}^{*} (A))$
3		ovoliun.a	$⊢ (φ \land n \in ℕ) \to A \subseteq ℝ$
4		ovoliun.v	$⊢ (φ \land n \in ℕ) \to {vol}^{*} (A) \in ℝ$
5		ovoliun.r	$⊢ φ \to sup (ran T ℝ^{*} <) \in ℝ$
6		ovoliun.b	$⊢ φ \to B \in ℝ^{+}$
7		ovoliun.s	$⊢ S = seq 1 (+ ((abs \circ -) \circ F (n)))$
8		ovoliun.u	$⊢ U = seq 1 (+ ((abs \circ -) \circ H))$
9		ovoliun.h	$⊢ H = (k \in ℕ ⟼ F (1^{st} (J (k))) (2^{nd} (J (k))))$
10		ovoliun.j	$⊢ φ \to J : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ$
11		ovoliun.f	$⊢ φ \to F : ℕ ⟶ {(\leq \cap ℝ^{2})}^{ℕ}$
12		ovoliun.x1	$⊢ (φ \land n \in ℕ) \to A \subseteq ⋃ ran ((.) \circ F (n))$
13		ovoliun.x2	$⊢ (φ \land n \in ℕ) \to sup (ran S ℝ^{} <) \leq {vol}^{} (A) + (\frac{B}{2^{n}})$
14	3	ralrimiva	$⊢ φ \to \forall n \in ℕ A \subseteq ℝ$
15		iunss	$⊢ ⋃_{n \in ℕ} A \subseteq ℝ \leftrightarrow \forall n \in ℕ A \subseteq ℝ$
16	14 15	sylibr	$⊢ φ \to ⋃_{n \in ℕ} A \subseteq ℝ$
17		ovolcl	$⊢ ⋃_{n \in ℕ} A \subseteq ℝ \to {vol}^{} (⋃_{n \in ℕ} A) \in ℝ^{}$
18	16 17	syl	$⊢ φ \to {vol}^{} (⋃_{n \in ℕ} A) \in ℝ^{}$
19	11	adantr	$⊢ (φ \land k \in ℕ) \to F : ℕ ⟶ {(\leq \cap ℝ^{2})}^{ℕ}$
20		f1of	$⊢ J : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ \to J : ℕ ⟶ ℕ \times ℕ$
21	10 20	syl	$⊢ φ \to J : ℕ ⟶ ℕ \times ℕ$
22	21	ffvelrnda	$⊢ (φ \land k \in ℕ) \to J (k) \in (ℕ \times ℕ)$
23		xp1st	$⊢ J (k) \in (ℕ \times ℕ) \to 1^{st} (J (k)) \in ℕ$
24	22 23	syl	$⊢ (φ \land k \in ℕ) \to 1^{st} (J (k)) \in ℕ$
25	19 24	ffvelrnd	$⊢ (φ \land k \in ℕ) \to F (1^{st} (J (k))) \in ({(\leq \cap ℝ^{2})}^{ℕ})$
26		elovolmlem	$⊢ F (1^{st} (J (k))) \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow F (1^{st} (J (k))) : ℕ ⟶ \leq \cap ℝ^{2}$
27	25 26	sylib	$⊢ (φ \land k \in ℕ) \to F (1^{st} (J (k))) : ℕ ⟶ \leq \cap ℝ^{2}$
28		xp2nd	$⊢ J (k) \in (ℕ \times ℕ) \to 2^{nd} (J (k)) \in ℕ$
29	22 28	syl	$⊢ (φ \land k \in ℕ) \to 2^{nd} (J (k)) \in ℕ$
30	27 29	ffvelrnd	$⊢ (φ \land k \in ℕ) \to F (1^{st} (J (k))) (2^{nd} (J (k))) \in (\leq \cap ℝ^{2})$
31	30 9	fmptd	$⊢ φ \to H : ℕ ⟶ \leq \cap ℝ^{2}$
32		eqid	$⊢ (abs \circ -) \circ H = (abs \circ -) \circ H$
33	32 8	ovolsf	$⊢ H : ℕ ⟶ \leq \cap ℝ^{2} \to U : ℕ ⟶ [0, +∞)$
34		frn	$⊢ U : ℕ ⟶ [0, +∞) \to ran U \subseteq [0, +∞)$
35	31 33 34	3syl	$⊢ φ \to ran U \subseteq [0, +∞)$
36		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
37	35 36	sstrdi	$⊢ φ \to ran U \subseteq ℝ^{*}$
38		supxrcl	$⊢ ran U \subseteq ℝ^{} \to sup (ran U ℝ^{} <) \in ℝ^{*}$
39	37 38	syl	$⊢ φ \to sup (ran U ℝ^{} <) \in ℝ^{}$
40	6	rpred	$⊢ φ \to B \in ℝ$
41	5 40	readdcld	$⊢ φ \to sup (ran T ℝ^{*} <) + B \in ℝ$
42	41	rexrd	$⊢ φ \to sup (ran T ℝ^{} <) + B \in ℝ^{}$
43		eliun	$⊢ z \in ⋃_{n \in ℕ} A \leftrightarrow \exists n \in ℕ z \in A$
44	12	3adant3	$⊢ (φ \land n \in ℕ \land z \in A) \to A \subseteq ⋃ ran ((.) \circ F (n))$
45	3	3adant3	$⊢ (φ \land n \in ℕ \land z \in A) \to A \subseteq ℝ$
46	11	ffvelrnda	$⊢ (φ \land n \in ℕ) \to F (n) \in ({(\leq \cap ℝ^{2})}^{ℕ})$
47		elovolmlem	$⊢ F (n) \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow F (n) : ℕ ⟶ \leq \cap ℝ^{2}$
48	46 47	sylib	$⊢ (φ \land n \in ℕ) \to F (n) : ℕ ⟶ \leq \cap ℝ^{2}$
49	48	3adant3	$⊢ (φ \land n \in ℕ \land z \in A) \to F (n) : ℕ ⟶ \leq \cap ℝ^{2}$
50		ovolfioo	$⊢ (A \subseteq ℝ \land F (n) : ℕ ⟶ \leq \cap ℝ^{2}) \to (A \subseteq ⋃ ran ((.) \circ F (n)) \leftrightarrow \forall z \in A \exists j \in ℕ (1^{st} (F (n) (j)) < z \land z < 2^{nd} (F (n) (j))))$
51	45 49 50	syl2anc	$⊢ (φ \land n \in ℕ \land z \in A) \to (A \subseteq ⋃ ran ((.) \circ F (n)) \leftrightarrow \forall z \in A \exists j \in ℕ (1^{st} (F (n) (j)) < z \land z < 2^{nd} (F (n) (j))))$
52	44 51	mpbid	$⊢ (φ \land n \in ℕ \land z \in A) \to \forall z \in A \exists j \in ℕ (1^{st} (F (n) (j)) < z \land z < 2^{nd} (F (n) (j)))$
53		simp3	$⊢ (φ \land n \in ℕ \land z \in A) \to z \in A$
54		rsp	$⊢ \forall z \in A \exists j \in ℕ (1^{st} (F (n) (j)) < z \land z < 2^{nd} (F (n) (j))) \to (z \in A \to \exists j \in ℕ (1^{st} (F (n) (j)) < z \land z < 2^{nd} (F (n) (j))))$
55	52 53 54	sylc	$⊢ (φ \land n \in ℕ \land z \in A) \to \exists j \in ℕ (1^{st} (F (n) (j)) < z \land z < 2^{nd} (F (n) (j)))$
56		simpl1	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to φ$
57		f1ocnv	$⊢ J : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ \to J^{-1} : ℕ \times ℕ \underset{1-1 onto}{⟶} ℕ$
58		f1of	$⊢ J^{-1} : ℕ \times ℕ \underset{1-1 onto}{⟶} ℕ \to J^{-1} : ℕ \times ℕ ⟶ ℕ$
59	56 10 57 58	4syl	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to J^{-1} : ℕ \times ℕ ⟶ ℕ$
60		simpl2	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to n \in ℕ$
61		simpr	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to j \in ℕ$
62	59 60 61	fovrnd	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to n J^{-1} j \in ℕ$
63		2fveq3	$⊢ k = n J^{-1} j \to 1^{st} (J (k)) = 1^{st} (J (n J^{-1} j))$
64	63	fveq2d	$⊢ k = n J^{-1} j \to F (1^{st} (J (k))) = F (1^{st} (J (n J^{-1} j)))$
65		2fveq3	$⊢ k = n J^{-1} j \to 2^{nd} (J (k)) = 2^{nd} (J (n J^{-1} j))$
66	64 65	fveq12d	$⊢ k = n J^{-1} j \to F (1^{st} (J (k))) (2^{nd} (J (k))) = F (1^{st} (J (n J^{-1} j))) (2^{nd} (J (n J^{-1} j)))$
67		fvex	$⊢ F (1^{st} (J (n J^{-1} j))) (2^{nd} (J (n J^{-1} j))) \in V$
68	66 9 67	fvmpt	$⊢ n J^{-1} j \in ℕ \to H (n J^{-1} j) = F (1^{st} (J (n J^{-1} j))) (2^{nd} (J (n J^{-1} j)))$
69	62 68	syl	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to H (n J^{-1} j) = F (1^{st} (J (n J^{-1} j))) (2^{nd} (J (n J^{-1} j)))$
70		df-ov	$⊢ n J^{-1} j = J^{-1} (⟨n, j⟩)$
71	70	fveq2i	$⊢ J (n J^{-1} j) = J (J^{-1} (⟨n, j⟩))$
72	56 10	syl	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to J : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ$
73	60 61	opelxpd	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to ⟨n, j⟩ \in (ℕ \times ℕ)$
74		f1ocnvfv2	$⊢ (J : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ \land ⟨n, j⟩ \in (ℕ \times ℕ)) \to J (J^{-1} (⟨n, j⟩)) = ⟨n, j⟩$
75	72 73 74	syl2anc	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to J (J^{-1} (⟨n, j⟩)) = ⟨n, j⟩$
76	71 75	eqtrid	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to J (n J^{-1} j) = ⟨n, j⟩$
77	76	fveq2d	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to 1^{st} (J (n J^{-1} j)) = 1^{st} (⟨n, j⟩)$
78		vex	$⊢ n \in V$
79		vex	$⊢ j \in V$
80	78 79	op1st	$⊢ 1^{st} (⟨n, j⟩) = n$
81	77 80	eqtrdi	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to 1^{st} (J (n J^{-1} j)) = n$
82	81	fveq2d	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to F (1^{st} (J (n J^{-1} j))) = F (n)$
83	76	fveq2d	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to 2^{nd} (J (n J^{-1} j)) = 2^{nd} (⟨n, j⟩)$
84	78 79	op2nd	$⊢ 2^{nd} (⟨n, j⟩) = j$
85	83 84	eqtrdi	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to 2^{nd} (J (n J^{-1} j)) = j$
86	82 85	fveq12d	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to F (1^{st} (J (n J^{-1} j))) (2^{nd} (J (n J^{-1} j))) = F (n) (j)$
87	69 86	eqtrd	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to H (n J^{-1} j) = F (n) (j)$
88	87	fveq2d	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to 1^{st} (H (n J^{-1} j)) = 1^{st} (F (n) (j))$
89	88	breq1d	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to (1^{st} (H (n J^{-1} j)) < z \leftrightarrow 1^{st} (F (n) (j)) < z)$
90	87	fveq2d	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to 2^{nd} (H (n J^{-1} j)) = 2^{nd} (F (n) (j))$
91	90	breq2d	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to (z < 2^{nd} (H (n J^{-1} j)) \leftrightarrow z < 2^{nd} (F (n) (j)))$
92	89 91	anbi12d	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to ((1^{st} (H (n J^{-1} j)) < z \land z < 2^{nd} (H (n J^{-1} j))) \leftrightarrow (1^{st} (F (n) (j)) < z \land z < 2^{nd} (F (n) (j))))$
93	92	biimprd	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to ((1^{st} (F (n) (j)) < z \land z < 2^{nd} (F (n) (j))) \to (1^{st} (H (n J^{-1} j)) < z \land z < 2^{nd} (H (n J^{-1} j))))$
94		2fveq3	$⊢ m = n J^{-1} j \to 1^{st} (H (m)) = 1^{st} (H (n J^{-1} j))$
95	94	breq1d	$⊢ m = n J^{-1} j \to (1^{st} (H (m)) < z \leftrightarrow 1^{st} (H (n J^{-1} j)) < z)$
96		2fveq3	$⊢ m = n J^{-1} j \to 2^{nd} (H (m)) = 2^{nd} (H (n J^{-1} j))$
97	96	breq2d	$⊢ m = n J^{-1} j \to (z < 2^{nd} (H (m)) \leftrightarrow z < 2^{nd} (H (n J^{-1} j)))$
98	95 97	anbi12d	$⊢ m = n J^{-1} j \to ((1^{st} (H (m)) < z \land z < 2^{nd} (H (m))) \leftrightarrow (1^{st} (H (n J^{-1} j)) < z \land z < 2^{nd} (H (n J^{-1} j))))$
99	98	rspcev	$⊢ (n J^{-1} j \in ℕ \land (1^{st} (H (n J^{-1} j)) < z \land z < 2^{nd} (H (n J^{-1} j)))) \to \exists m \in ℕ (1^{st} (H (m)) < z \land z < 2^{nd} (H (m)))$
100	62 93 99	syl6an	$⊢ ((φ \land n \in ℕ \land z \in A) \land j \in ℕ) \to ((1^{st} (F (n) (j)) < z \land z < 2^{nd} (F (n) (j))) \to \exists m \in ℕ (1^{st} (H (m)) < z \land z < 2^{nd} (H (m))))$
101	100	rexlimdva	$⊢ (φ \land n \in ℕ \land z \in A) \to (\exists j \in ℕ (1^{st} (F (n) (j)) < z \land z < 2^{nd} (F (n) (j))) \to \exists m \in ℕ (1^{st} (H (m)) < z \land z < 2^{nd} (H (m))))$
102	55 101	mpd	$⊢ (φ \land n \in ℕ \land z \in A) \to \exists m \in ℕ (1^{st} (H (m)) < z \land z < 2^{nd} (H (m)))$
103	102	rexlimdv3a	$⊢ φ \to (\exists n \in ℕ z \in A \to \exists m \in ℕ (1^{st} (H (m)) < z \land z < 2^{nd} (H (m))))$
104	43 103	syl5bi	$⊢ φ \to (z \in ⋃_{n \in ℕ} A \to \exists m \in ℕ (1^{st} (H (m)) < z \land z < 2^{nd} (H (m))))$
105	104	ralrimiv	$⊢ φ \to \forall z \in ⋃_{n \in ℕ} A \exists m \in ℕ (1^{st} (H (m)) < z \land z < 2^{nd} (H (m)))$
106		ovolfioo	$⊢ (⋃_{n \in ℕ} A \subseteq ℝ \land H : ℕ ⟶ \leq \cap ℝ^{2}) \to (⋃_{n \in ℕ} A \subseteq ⋃ ran ((.) \circ H) \leftrightarrow \forall z \in ⋃_{n \in ℕ} A \exists m \in ℕ (1^{st} (H (m)) < z \land z < 2^{nd} (H (m))))$
107	16 31 106	syl2anc	$⊢ φ \to (⋃_{n \in ℕ} A \subseteq ⋃ ran ((.) \circ H) \leftrightarrow \forall z \in ⋃_{n \in ℕ} A \exists m \in ℕ (1^{st} (H (m)) < z \land z < 2^{nd} (H (m))))$
108	105 107	mpbird	$⊢ φ \to ⋃_{n \in ℕ} A \subseteq ⋃ ran ((.) \circ H)$
109	8	ovollb	$⊢ (H : ℕ ⟶ \leq \cap ℝ^{2} \land ⋃_{n \in ℕ} A \subseteq ⋃ ran ((.) \circ H)) \to {vol}^{} (⋃_{n \in ℕ} A) \leq sup (ran U ℝ^{} <)$
110	31 108 109	syl2anc	$⊢ φ \to {vol}^{} (⋃_{n \in ℕ} A) \leq sup (ran U ℝ^{} <)$
111		fzfi	$⊢ (1 \dots j) \in Fin$
112		elfznn	$⊢ w \in (1 \dots j) \to w \in ℕ$
113		ffvelrn	$⊢ (J : ℕ ⟶ ℕ \times ℕ \land w \in ℕ) \to J (w) \in (ℕ \times ℕ)$
114		xp1st	$⊢ J (w) \in (ℕ \times ℕ) \to 1^{st} (J (w)) \in ℕ$
115		nnre	$⊢ 1^{st} (J (w)) \in ℕ \to 1^{st} (J (w)) \in ℝ$
116	113 114 115	3syl	$⊢ (J : ℕ ⟶ ℕ \times ℕ \land w \in ℕ) \to 1^{st} (J (w)) \in ℝ$
117	21 112 116	syl2an	$⊢ (φ \land w \in (1 \dots j)) \to 1^{st} (J (w)) \in ℝ$
118	117	ralrimiva	$⊢ φ \to \forall w \in (1 \dots j) 1^{st} (J (w)) \in ℝ$
119	118	adantr	$⊢ (φ \land j \in ℕ) \to \forall w \in (1 \dots j) 1^{st} (J (w)) \in ℝ$
120		fimaxre3	$⊢ ((1 \dots j) \in Fin \land \forall w \in (1 \dots j) 1^{st} (J (w)) \in ℝ) \to \exists x \in ℝ \forall w \in (1 \dots j) 1^{st} (J (w)) \leq x$
121	111 119 120	sylancr	$⊢ (φ \land j \in ℕ) \to \exists x \in ℝ \forall w \in (1 \dots j) 1^{st} (J (w)) \leq x$
122		fllep1	$⊢ x \in ℝ \to x \leq ⌊x⌋ + 1$
123	122	ad2antlr	$⊢ ((φ \land x \in ℝ) \land w \in (1 \dots j)) \to x \leq ⌊x⌋ + 1$
124	117	adantlr	$⊢ ((φ \land x \in ℝ) \land w \in (1 \dots j)) \to 1^{st} (J (w)) \in ℝ$
125		simplr	$⊢ ((φ \land x \in ℝ) \land w \in (1 \dots j)) \to x \in ℝ$
126		flcl	$⊢ x \in ℝ \to ⌊x⌋ \in ℤ$
127	126	peano2zd	$⊢ x \in ℝ \to ⌊x⌋ + 1 \in ℤ$
128	127	zred	$⊢ x \in ℝ \to ⌊x⌋ + 1 \in ℝ$
129	128	ad2antlr	$⊢ ((φ \land x \in ℝ) \land w \in (1 \dots j)) \to ⌊x⌋ + 1 \in ℝ$
130		letr	$⊢ (1^{st} (J (w)) \in ℝ \land x \in ℝ \land ⌊x⌋ + 1 \in ℝ) \to ((1^{st} (J (w)) \leq x \land x \leq ⌊x⌋ + 1) \to 1^{st} (J (w)) \leq ⌊x⌋ + 1)$
131	124 125 129 130	syl3anc	$⊢ ((φ \land x \in ℝ) \land w \in (1 \dots j)) \to ((1^{st} (J (w)) \leq x \land x \leq ⌊x⌋ + 1) \to 1^{st} (J (w)) \leq ⌊x⌋ + 1)$
132	123 131	mpan2d	$⊢ ((φ \land x \in ℝ) \land w \in (1 \dots j)) \to (1^{st} (J (w)) \leq x \to 1^{st} (J (w)) \leq ⌊x⌋ + 1)$
133	132	ralimdva	$⊢ (φ \land x \in ℝ) \to (\forall w \in (1 \dots j) 1^{st} (J (w)) \leq x \to \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)$
134	133	adantlr	$⊢ ((φ \land j \in ℕ) \land x \in ℝ) \to (\forall w \in (1 \dots j) 1^{st} (J (w)) \leq x \to \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)$
135		simpll	$⊢ ((φ \land j \in ℕ) \land (x \in ℝ \land \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)) \to φ$
136	135 3	sylan	$⊢ (((φ \land j \in ℕ) \land (x \in ℝ \land \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)) \land n \in ℕ) \to A \subseteq ℝ$
137	135 4	sylan	$⊢ (((φ \land j \in ℕ) \land (x \in ℝ \land \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)) \land n \in ℕ) \to {vol}^{*} (A) \in ℝ$
138	135 5	syl	$⊢ ((φ \land j \in ℕ) \land (x \in ℝ \land \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)) \to sup (ran T ℝ^{*} <) \in ℝ$
139	135 6	syl	$⊢ ((φ \land j \in ℕ) \land (x \in ℝ \land \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)) \to B \in ℝ^{+}$
140	135 10	syl	$⊢ ((φ \land j \in ℕ) \land (x \in ℝ \land \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)) \to J : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ$
141	135 11	syl	$⊢ ((φ \land j \in ℕ) \land (x \in ℝ \land \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)) \to F : ℕ ⟶ {(\leq \cap ℝ^{2})}^{ℕ}$
142	135 12	sylan	$⊢ (((φ \land j \in ℕ) \land (x \in ℝ \land \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)) \land n \in ℕ) \to A \subseteq ⋃ ran ((.) \circ F (n))$
143	135 13	sylan	$⊢ (((φ \land j \in ℕ) \land (x \in ℝ \land \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)) \land n \in ℕ) \to sup (ran S ℝ^{} <) \leq {vol}^{} (A) + (\frac{B}{2^{n}})$
144		simplr	$⊢ ((φ \land j \in ℕ) \land (x \in ℝ \land \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)) \to j \in ℕ$
145	127	ad2antrl	$⊢ ((φ \land j \in ℕ) \land (x \in ℝ \land \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)) \to ⌊x⌋ + 1 \in ℤ$
146		simprr	$⊢ ((φ \land j \in ℕ) \land (x \in ℝ \land \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)) \to \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1$
147	1 2 136 137 138 139 7 8 9 140 141 142 143 144 145 146	ovoliunlem1	$⊢ ((φ \land j \in ℕ) \land (x \in ℝ \land \forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1)) \to U (j) \leq sup (ran T ℝ^{*} <) + B$
148	147	expr	$⊢ ((φ \land j \in ℕ) \land x \in ℝ) \to (\forall w \in (1 \dots j) 1^{st} (J (w)) \leq ⌊x⌋ + 1 \to U (j) \leq sup (ran T ℝ^{*} <) + B)$
149	134 148	syld	$⊢ ((φ \land j \in ℕ) \land x \in ℝ) \to (\forall w \in (1 \dots j) 1^{st} (J (w)) \leq x \to U (j) \leq sup (ran T ℝ^{*} <) + B)$
150	149	rexlimdva	$⊢ (φ \land j \in ℕ) \to (\exists x \in ℝ \forall w \in (1 \dots j) 1^{st} (J (w)) \leq x \to U (j) \leq sup (ran T ℝ^{*} <) + B)$
151	121 150	mpd	$⊢ (φ \land j \in ℕ) \to U (j) \leq sup (ran T ℝ^{*} <) + B$
152	151	ralrimiva	$⊢ φ \to \forall j \in ℕ U (j) \leq sup (ran T ℝ^{*} <) + B$
153		ffn	$⊢ U : ℕ ⟶ [0, +∞) \to U Fn ℕ$
154		breq1	$⊢ z = U (j) \to (z \leq sup (ran T ℝ^{} <) + B \leftrightarrow U (j) \leq sup (ran T ℝ^{} <) + B)$
155	154	ralrn	$⊢ U Fn ℕ \to (\forall z \in ran U z \leq sup (ran T ℝ^{} <) + B \leftrightarrow \forall j \in ℕ U (j) \leq sup (ran T ℝ^{} <) + B)$
156	31 33 153 155	4syl	$⊢ φ \to (\forall z \in ran U z \leq sup (ran T ℝ^{} <) + B \leftrightarrow \forall j \in ℕ U (j) \leq sup (ran T ℝ^{} <) + B)$
157	152 156	mpbird	$⊢ φ \to \forall z \in ran U z \leq sup (ran T ℝ^{*} <) + B$
158		supxrleub	$⊢ (ran U \subseteq ℝ^{} \land sup (ran T ℝ^{} <) + B \in ℝ^{}) \to (sup (ran U ℝ^{} <) \leq sup (ran T ℝ^{} <) + B \leftrightarrow \forall z \in ran U z \leq sup (ran T ℝ^{} <) + B)$
159	37 42 158	syl2anc	$⊢ φ \to (sup (ran U ℝ^{} <) \leq sup (ran T ℝ^{} <) + B \leftrightarrow \forall z \in ran U z \leq sup (ran T ℝ^{*} <) + B)$
160	157 159	mpbird	$⊢ φ \to sup (ran U ℝ^{} <) \leq sup (ran T ℝ^{} <) + B$
161	18 39 42 110 160	xrletrd	$⊢ φ \to {vol}^{} (⋃_{n \in ℕ} A) \leq sup (ran T ℝ^{} <) + B$

Metamath Proof Explorer

Theorem ovoliunlem2

Proof