Theorem uniioombllem1

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 25-Mar-2015)

	Ref	Expression
Hypotheses	uniioombl.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
	uniioombl.2	⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
	uniioombl.3	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
	uniioombl.a	⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 )
	uniioombl.e	⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
	uniioombl.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
	uniioombl.g	⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
	uniioombl.s	⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
	uniioombl.t	⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
	uniioombl.v	⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
Assertion	uniioombllem1	⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		uniioombl.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2		uniioombl.2	⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
3		uniioombl.3	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
4		uniioombl.a	⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 )
5		uniioombl.e	⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
6		uniioombl.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
7		uniioombl.g	⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
8		uniioombl.s	⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
9		uniioombl.t	⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
10		uniioombl.v	⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
11		eqid	⊢ ( ( abs ∘ − ) ∘ 𝐺 ) = ( ( abs ∘ − ) ∘ 𝐺 )
12	11 9	ovolsf	⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) )
13	7 12	syl	⊢ ( 𝜑 → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) )
14	13	frnd	⊢ ( 𝜑 → ran 𝑇 ⊆ ( 0 [,) +∞ ) )
15		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
16	14 15	sstrdi	⊢ ( 𝜑 → ran 𝑇 ⊆ ℝ )
17		1nn	⊢ 1 ∈ ℕ
18	13	fdmd	⊢ ( 𝜑 → dom 𝑇 = ℕ )
19	17 18	eleqtrrid	⊢ ( 𝜑 → 1 ∈ dom 𝑇 )
20	19	ne0d	⊢ ( 𝜑 → dom 𝑇 ≠ ∅ )
21		dm0rn0	⊢ ( dom 𝑇 = ∅ ↔ ran 𝑇 = ∅ )
22	21	necon3bii	⊢ ( dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅ )
23	20 22	sylib	⊢ ( 𝜑 → ran 𝑇 ≠ ∅ )
24		icossxr	⊢ ( 0 [,) +∞ ) ⊆ ℝ*
25	14 24	sstrdi	⊢ ( 𝜑 → ran 𝑇 ⊆ ℝ* )
26		supxrcl	⊢ ( ran 𝑇 ⊆ ℝ* → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ* )
27	25 26	syl	⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ* )
28	6	rpred	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
29	5 28	readdcld	⊢ ( 𝜑 → ( ( vol* ‘ 𝐸 ) + 𝐶 ) ∈ ℝ )
30	29	rexrd	⊢ ( 𝜑 → ( ( vol* ‘ 𝐸 ) + 𝐶 ) ∈ ℝ* )
31		pnfxr	⊢ +∞ ∈ ℝ*
32	31	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ* )
33	29	ltpnfd	⊢ ( 𝜑 → ( ( vol* ‘ 𝐸 ) + 𝐶 ) < +∞ )
34	27 30 32 10 33	xrlelttrd	⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) < +∞ )
35		supxrbnd	⊢ ( ( ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ sup ( ran 𝑇 , ℝ* , < ) < +∞ ) → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )
36	16 23 34 35	syl3anc	⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )