ovoliunlem2

	Ref	Expression
Hypotheses	ovoliun.t	⊢ 𝑇 = seq 1 ( + , 𝐺 )
	ovoliun.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ 𝐴 ) )
	ovoliun.a	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ℝ )
	ovoliun.v	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
	ovoliun.r	⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ^* , < ) ∈ ℝ )
	ovoliun.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ⁺ )
	ovoliun.s	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) ) )
	ovoliun.u	⊢ 𝑈 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) )
	ovoliun.h	⊢ 𝐻 = ( 𝑘 ∈ ℕ ↦ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑘 ) ) ) )
	ovoliun.j	⊢ ( 𝜑 → 𝐽 : ℕ –1-1-onto→ ( ℕ × ℕ ) )
	ovoliun.f	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
	ovoliun.x1	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝐹 ‘ 𝑛 ) ) )
	ovoliun.x2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → sup ( ran 𝑆 , ℝ^* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) )
Assertion	ovoliunlem2	⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ovoliun.t	⊢ 𝑇 = seq 1 ( + , 𝐺 )
2		ovoliun.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ 𝐴 ) )
3		ovoliun.a	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ℝ )
4		ovoliun.v	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
5		ovoliun.r	⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ^* , < ) ∈ ℝ )
6		ovoliun.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ⁺ )
7		ovoliun.s	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝐹 ‘ 𝑛 ) ) )
8		ovoliun.u	⊢ 𝑈 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) )
9		ovoliun.h	⊢ 𝐻 = ( 𝑘 ∈ ℕ ↦ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑘 ) ) ) )
10		ovoliun.j	⊢ ( 𝜑 → 𝐽 : ℕ –1-1-onto→ ( ℕ × ℕ ) )
11		ovoliun.f	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
12		ovoliun.x1	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝐹 ‘ 𝑛 ) ) )
13		ovoliun.x2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → sup ( ran 𝑆 , ℝ^* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) )
14	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ )
15		iunss	⊢ ( ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ ↔ ∀ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ )
16	14 15	sylibr	⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ )
17		ovolcl	⊢ ( ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ → ( vol* ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ∈ ℝ^* )
18	16 17	syl	⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ∈ ℝ^* )
19	11	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
20		f1of	⊢ ( 𝐽 : ℕ –1-1-onto→ ( ℕ × ℕ ) → 𝐽 : ℕ ⟶ ( ℕ × ℕ ) )
21	10 20	syl	⊢ ( 𝜑 → 𝐽 : ℕ ⟶ ( ℕ × ℕ ) )
22	21	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐽 ‘ 𝑘 ) ∈ ( ℕ × ℕ ) )
23		xp1st	⊢ ( ( 𝐽 ‘ 𝑘 ) ∈ ( ℕ × ℕ ) → ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ∈ ℕ )
24	22 23	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ∈ ℕ )
25	19 24	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
26		elovolmlem	⊢ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ↔ ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
27	25 26	sylib	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
28		xp2nd	⊢ ( ( 𝐽 ‘ 𝑘 ) ∈ ( ℕ × ℕ ) → ( 2^nd ‘ ( 𝐽 ‘ 𝑘 ) ) ∈ ℕ )
29	22 28	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2^nd ‘ ( 𝐽 ‘ 𝑘 ) ) ∈ ℕ )
30	27 29	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑘 ) ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
31	30 9	fmptd	⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
32		eqid	⊢ ( ( abs ∘ − ) ∘ 𝐻 ) = ( ( abs ∘ − ) ∘ 𝐻 )
33	32 8	ovolsf	⊢ ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑈 : ℕ ⟶ ( 0 [,) +∞ ) )
34		frn	⊢ ( 𝑈 : ℕ ⟶ ( 0 [,) +∞ ) → ran 𝑈 ⊆ ( 0 [,) +∞ ) )
35	31 33 34	3syl	⊢ ( 𝜑 → ran 𝑈 ⊆ ( 0 [,) +∞ ) )
36		icossxr	⊢ ( 0 [,) +∞ ) ⊆ ℝ^*
37	35 36	sstrdi	⊢ ( 𝜑 → ran 𝑈 ⊆ ℝ^* )
38		supxrcl	⊢ ( ran 𝑈 ⊆ ℝ^* → sup ( ran 𝑈 , ℝ^* , < ) ∈ ℝ^* )
39	37 38	syl	⊢ ( 𝜑 → sup ( ran 𝑈 , ℝ^* , < ) ∈ ℝ^* )
40	6	rpred	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
41	5 40	readdcld	⊢ ( 𝜑 → ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ∈ ℝ )
42	41	rexrd	⊢ ( 𝜑 → ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ∈ ℝ^* )
43		eliun	⊢ ( 𝑧 ∈ ∪ 𝑛 ∈ ℕ 𝐴 ↔ ∃ 𝑛 ∈ ℕ 𝑧 ∈ 𝐴 )
44	12	3adant3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) → 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝐹 ‘ 𝑛 ) ) )
45	3	3adant3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) → 𝐴 ⊆ ℝ )
46	11	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
47		elovolmlem	⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ↔ ( 𝐹 ‘ 𝑛 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
48	46 47	sylib	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
49	48	3adant3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑛 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
50		ovolfioo	⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝐹 ‘ 𝑛 ) : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝐹 ‘ 𝑛 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑗 ∈ ℕ ( ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) ) ) )
51	45 49 50	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝐹 ‘ 𝑛 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑗 ∈ ℕ ( ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) ) ) )
52	44 51	mpbid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑗 ∈ ℕ ( ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) ) )
53		simp3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
54		rsp	⊢ ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑗 ∈ ℕ ( ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) ) → ( 𝑧 ∈ 𝐴 → ∃ 𝑗 ∈ ℕ ( ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) ) ) )
55	52 53 54	sylc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑗 ∈ ℕ ( ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) ) )
56		simpl1	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → 𝜑 )
57		f1ocnv	⊢ ( 𝐽 : ℕ –1-1-onto→ ( ℕ × ℕ ) → ^◡ 𝐽 : ( ℕ × ℕ ) –1-1-onto→ ℕ )
58		f1of	⊢ ( ^◡ 𝐽 : ( ℕ × ℕ ) –1-1-onto→ ℕ → ^◡ 𝐽 : ( ℕ × ℕ ) ⟶ ℕ )
59	56 10 57 58	4syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ^◡ 𝐽 : ( ℕ × ℕ ) ⟶ ℕ )
60		simpl2	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → 𝑛 ∈ ℕ )
61		simpr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
62	59 60 61	fovcdmd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑛 ^◡ 𝐽 𝑗 ) ∈ ℕ )
63		2fveq3	⊢ ( 𝑘 = ( 𝑛 ^◡ 𝐽 𝑗 ) → ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) = ( 1^st ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) )
64	63	fveq2d	⊢ ( 𝑘 = ( 𝑛 ^◡ 𝐽 𝑗 ) → ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) )
65		2fveq3	⊢ ( 𝑘 = ( 𝑛 ^◡ 𝐽 𝑗 ) → ( 2^nd ‘ ( 𝐽 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) )
66	64 65	fveq12d	⊢ ( 𝑘 = ( 𝑛 ^◡ 𝐽 𝑗 ) → ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ 𝑘 ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ 𝑘 ) ) ) = ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) )
67		fvex	⊢ ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) ∈ V
68	66 9 67	fvmpt	⊢ ( ( 𝑛 ^◡ 𝐽 𝑗 ) ∈ ℕ → ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) = ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) )
69	62 68	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) = ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) )
70		df-ov	⊢ ( 𝑛 ^◡ 𝐽 𝑗 ) = ( ^◡ 𝐽 ‘ ⟨ 𝑛 , 𝑗 ⟩ )
71	70	fveq2i	⊢ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) = ( 𝐽 ‘ ( ^◡ 𝐽 ‘ ⟨ 𝑛 , 𝑗 ⟩ ) )
72	56 10	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → 𝐽 : ℕ –1-1-onto→ ( ℕ × ℕ ) )
73	60 61	opelxpd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ⟨ 𝑛 , 𝑗 ⟩ ∈ ( ℕ × ℕ ) )
74		f1ocnvfv2	⊢ ( ( 𝐽 : ℕ –1-1-onto→ ( ℕ × ℕ ) ∧ ⟨ 𝑛 , 𝑗 ⟩ ∈ ( ℕ × ℕ ) ) → ( 𝐽 ‘ ( ^◡ 𝐽 ‘ ⟨ 𝑛 , 𝑗 ⟩ ) ) = ⟨ 𝑛 , 𝑗 ⟩ )
75	72 73 74	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( 𝐽 ‘ ( ^◡ 𝐽 ‘ ⟨ 𝑛 , 𝑗 ⟩ ) ) = ⟨ 𝑛 , 𝑗 ⟩ )
76	71 75	eqtrid	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) = ⟨ 𝑛 , 𝑗 ⟩ )
77	76	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( 1^st ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) = ( 1^st ‘ ⟨ 𝑛 , 𝑗 ⟩ ) )
78		vex	⊢ 𝑛 ∈ V
79		vex	⊢ 𝑗 ∈ V
80	78 79	op1st	⊢ ( 1^st ‘ ⟨ 𝑛 , 𝑗 ⟩ ) = 𝑛
81	77 80	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( 1^st ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) = 𝑛 )
82	81	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) = ( 𝐹 ‘ 𝑛 ) )
83	76	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( 2^nd ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) = ( 2^nd ‘ ⟨ 𝑛 , 𝑗 ⟩ ) )
84	78 79	op2nd	⊢ ( 2^nd ‘ ⟨ 𝑛 , 𝑗 ⟩ ) = 𝑗
85	83 84	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( 2^nd ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) = 𝑗 )
86	82 85	fveq12d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( 1^st ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) ‘ ( 2^nd ‘ ( 𝐽 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) )
87	69 86	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) )
88	87	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( 1^st ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) = ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) )
89	88	breq1d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) < 𝑧 ↔ ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) < 𝑧 ) )
90	87	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( 2^nd ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) = ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) )
91	90	breq2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ↔ 𝑧 < ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) ) )
92	89 91	anbi12d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( ( ( 1^st ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) ↔ ( ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) ) ) )
93	92	biimprd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( ( ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) ) → ( ( 1^st ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) ) )
94		2fveq3	⊢ ( 𝑚 = ( 𝑛 ^◡ 𝐽 𝑗 ) → ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) = ( 1^st ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) )
95	94	breq1d	⊢ ( 𝑚 = ( 𝑛 ^◡ 𝐽 𝑗 ) → ( ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) < 𝑧 ↔ ( 1^st ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) < 𝑧 ) )
96		2fveq3	⊢ ( 𝑚 = ( 𝑛 ^◡ 𝐽 𝑗 ) → ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) = ( 2^nd ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) )
97	96	breq2d	⊢ ( 𝑚 = ( 𝑛 ^◡ 𝐽 𝑗 ) → ( 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) ↔ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) )
98	95 97	anbi12d	⊢ ( 𝑚 = ( 𝑛 ^◡ 𝐽 𝑗 ) → ( ( ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) ) ↔ ( ( 1^st ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) ) )
99	98	rspcev	⊢ ( ( ( 𝑛 ^◡ 𝐽 𝑗 ) ∈ ℕ ∧ ( ( 1^st ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ ( 𝑛 ^◡ 𝐽 𝑗 ) ) ) ) ) → ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) ) )
100	62 93 99	syl6an	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑗 ∈ ℕ ) → ( ( ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) ) → ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) ) ) )
101	100	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑗 ∈ ℕ ( ( 1^st ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑗 ) ) ) → ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) ) ) )
102	55 101	mpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) ) )
103	102	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ 𝑧 ∈ 𝐴 → ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) ) ) )
104	43 103	biimtrid	⊢ ( 𝜑 → ( 𝑧 ∈ ∪ 𝑛 ∈ ℕ 𝐴 → ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) ) ) )
105	104	ralrimiv	⊢ ( 𝜑 → ∀ 𝑧 ∈ ∪ 𝑛 ∈ ℕ 𝐴 ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) ) )
106		ovolfioo	⊢ ( ( ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ ∧ 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐻 ) ↔ ∀ 𝑧 ∈ ∪ 𝑛 ∈ ℕ 𝐴 ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) ) ) )
107	16 31 106	syl2anc	⊢ ( 𝜑 → ( ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐻 ) ↔ ∀ 𝑧 ∈ ∪ 𝑛 ∈ ℕ 𝐴 ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐻 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐻 ‘ 𝑚 ) ) ) ) )
108	105 107	mpbird	⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐻 ) )
109	8	ovollb	⊢ ( ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐻 ) ) → ( vol* ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ≤ sup ( ran 𝑈 , ℝ^* , < ) )
110	31 108 109	syl2anc	⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ≤ sup ( ran 𝑈 , ℝ^* , < ) )
111		fzfi	⊢ ( 1 ... 𝑗 ) ∈ Fin
112		elfznn	⊢ ( 𝑤 ∈ ( 1 ... 𝑗 ) → 𝑤 ∈ ℕ )
113		ffvelcdm	⊢ ( ( 𝐽 : ℕ ⟶ ( ℕ × ℕ ) ∧ 𝑤 ∈ ℕ ) → ( 𝐽 ‘ 𝑤 ) ∈ ( ℕ × ℕ ) )
114		xp1st	⊢ ( ( 𝐽 ‘ 𝑤 ) ∈ ( ℕ × ℕ ) → ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ∈ ℕ )
115		nnre	⊢ ( ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ∈ ℕ → ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ∈ ℝ )
116	113 114 115	3syl	⊢ ( ( 𝐽 : ℕ ⟶ ( ℕ × ℕ ) ∧ 𝑤 ∈ ℕ ) → ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ∈ ℝ )
117	21 112 116	syl2an	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 1 ... 𝑗 ) ) → ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ∈ ℝ )
118	117	ralrimiva	⊢ ( 𝜑 → ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ∈ ℝ )
119	118	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ∈ ℝ )
120		fimaxre3	⊢ ( ( ( 1 ... 𝑗 ) ∈ Fin ∧ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝑥 )
121	111 119 120	sylancr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝑥 )
122		fllep1	⊢ ( 𝑥 ∈ ℝ → 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) )
123	122	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑤 ∈ ( 1 ... 𝑗 ) ) → 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) )
124	117	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑤 ∈ ( 1 ... 𝑗 ) ) → ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ∈ ℝ )
125		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑤 ∈ ( 1 ... 𝑗 ) ) → 𝑥 ∈ ℝ )
126		flcl	⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ∈ ℤ )
127	126	peano2zd	⊢ ( 𝑥 ∈ ℝ → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℤ )
128	127	zred	⊢ ( 𝑥 ∈ ℝ → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ )
129	128	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑤 ∈ ( 1 ... 𝑗 ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ )
130		letr	⊢ ( ( ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ ) → ( ( ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) → ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
131	124 125 129 130	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑤 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) → ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
132	123 131	mpan2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑤 ∈ ( 1 ... 𝑗 ) ) → ( ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝑥 → ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
133	132	ralimdva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝑥 → ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
134	133	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝑥 → ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
135		simpll	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝜑 )
136	135 3	sylan	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ℝ )
137	135 4	sylan	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
138	135 5	syl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → sup ( ran 𝑇 , ℝ^* , < ) ∈ ℝ )
139	135 6	syl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝐵 ∈ ℝ⁺ )
140	135 10	syl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝐽 : ℕ –1-1-onto→ ( ℕ × ℕ ) )
141	135 11	syl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝐹 : ℕ ⟶ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
142	135 12	sylan	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ∪ ran ( (,) ∘ ( 𝐹 ‘ 𝑛 ) ) )
143	135 13	sylan	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ∧ 𝑛 ∈ ℕ ) → sup ( ran 𝑆 , ℝ^* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐵 / ( 2 ↑ 𝑛 ) ) ) )
144		simplr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑗 ∈ ℕ )
145	127	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℤ )
146		simprr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) )
147	1 2 136 137 138 139 7 8 9 140 141 142 143 144 145 146	ovoliunlem1	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( 𝑈 ‘ 𝑗 ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) )
148	147	expr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( 𝑈 ‘ 𝑗 ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ) )
149	134 148	syld	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝑥 → ( 𝑈 ‘ 𝑗 ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ) )
150	149	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ ( 1 ... 𝑗 ) ( 1^st ‘ ( 𝐽 ‘ 𝑤 ) ) ≤ 𝑥 → ( 𝑈 ‘ 𝑗 ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ) )
151	121 150	mpd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑈 ‘ 𝑗 ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) )
152	151	ralrimiva	⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) )
153		ffn	⊢ ( 𝑈 : ℕ ⟶ ( 0 [,) +∞ ) → 𝑈 Fn ℕ )
154		breq1	⊢ ( 𝑧 = ( 𝑈 ‘ 𝑗 ) → ( 𝑧 ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ↔ ( 𝑈 ‘ 𝑗 ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ) )
155	154	ralrn	⊢ ( 𝑈 Fn ℕ → ( ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ↔ ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ) )
156	31 33 153 155	4syl	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ↔ ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ) )
157	152 156	mpbird	⊢ ( 𝜑 → ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) )
158		supxrleub	⊢ ( ( ran 𝑈 ⊆ ℝ^* ∧ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ∈ ℝ^* ) → ( sup ( ran 𝑈 , ℝ^* , < ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ↔ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ) )
159	37 42 158	syl2anc	⊢ ( 𝜑 → ( sup ( ran 𝑈 , ℝ^* , < ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ↔ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) ) )
160	157 159	mpbird	⊢ ( 𝜑 → sup ( ran 𝑈 , ℝ^* , < ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) )
161	18 39 42 110 160	xrletrd	⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ^* , < ) + 𝐵 ) )

Metamath Proof Explorer

Theorem ovoliunlem2

Proof