This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ovolre

Description: The measure of the real numbers. (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Assertion ovolre ( vol* ‘ ℝ ) = +∞

Proof

Step Hyp Ref Expression
1 ssid ⊢ ℝ ⊆ ℝ
2 ovolcl ⊢ ( ℝ ⊆ ℝ → ( vol* ‘ ℝ ) ∈ ℝ* )
3 1 2 ax-mp ⊢ ( vol* ‘ ℝ ) ∈ ℝ*
4 pnfge ⊢ ( ( vol* ‘ ℝ ) ∈ ℝ* → ( vol* ‘ ℝ ) ≤ +∞ )
5 3 4 ax-mp ⊢ ( vol* ‘ ℝ ) ≤ +∞
6 0re ⊢ 0 ∈ ℝ
7 ovolicopnf ⊢ ( 0 ∈ ℝ → ( vol* ‘ ( 0 [,) +∞ ) ) = +∞ )
8 6 7 ax-mp ⊢ ( vol* ‘ ( 0 [,) +∞ ) ) = +∞
9 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
10 ovolss ⊢ ( ( ( 0 [,) +∞ ) ⊆ ℝ ∧ ℝ ⊆ ℝ ) → ( vol* ‘ ( 0 [,) +∞ ) ) ≤ ( vol* ‘ ℝ ) )
11 9 1 10 mp2an ⊢ ( vol* ‘ ( 0 [,) +∞ ) ) ≤ ( vol* ‘ ℝ )
12 8 11 eqbrtrri ⊢ +∞ ≤ ( vol* ‘ ℝ )
13 pnfxr ⊢ +∞ ∈ ℝ*
14 xrletri3 ⊢ ( ( ( vol* ‘ ℝ ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( vol* ‘ ℝ ) = +∞ ↔ ( ( vol* ‘ ℝ ) ≤ +∞ ∧ +∞ ≤ ( vol* ‘ ℝ ) ) ) )
15 3 13 14 mp2an ⊢ ( ( vol* ‘ ℝ ) = +∞ ↔ ( ( vol* ‘ ℝ ) ≤ +∞ ∧ +∞ ≤ ( vol* ‘ ℝ ) ) )
16 5 12 15 mpbir2an ⊢ ( vol* ‘ ℝ ) = +∞