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 ⊢01⊆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+∞→01⊆0+∞
12 1 10 11 mp2an ⊢01⊆0+∞