Metamath Proof Explorer

Theorem unitssxrge0

Description: The closed unit interval is a subset of the set of the extended nonnegative reals. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 12-Dec-2016)

Ref Expression
Assertion unitssxrge0 ⊢ 0 1 ⊆ 0 +∞

Proof

Step Hyp Ref Expression
1 0e0iccpnf ⊢ 0 ∈ 0 +∞
2 1xr ⊢ 1 ∈ ℝ *
3 0le1 ⊢ 0 ≤ 1
4 pnfge ⊢ 1 ∈ ℝ * → 1 ≤ +∞
5 2 4 ax-mp ⊢ 1 ≤ +∞
6 0xr ⊢ 0 ∈ ℝ *
7 pnfxr ⊢ +∞ ∈ ℝ *
8 elicc1 ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * → 1 ∈ 0 +∞ ↔ 1 ∈ ℝ * ∧ 0 ≤ 1 ∧ 1 ≤ +∞
9 6 7 8 mp2an ⊢ 1 ∈ 0 +∞ ↔ 1 ∈ ℝ * ∧ 0 ≤ 1 ∧ 1 ≤ +∞
10 2 3 5 9 mpbir3an ⊢ 1 ∈ 0 +∞
11 iccss2 ⊢ 0 ∈ 0 +∞ ∧ 1 ∈ 0 +∞ → 0 1 ⊆ 0 +∞
12 1 10 11 mp2an ⊢ 0 1 ⊆ 0 +∞