Metamath Proof Explorer

Theorem 1elunit

Description: One is an element of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013)

Ref Expression
Assertion 1elunit 
|- 1 e. ( 0 [,] 1 )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 0le1 
 |-  0 <_ 1
3 1le1 
 |-  1 <_ 1
4 elicc01 
 |-  ( 1 e. ( 0 [,] 1 ) <-> ( 1 e. RR /\ 0 <_ 1 /\ 1 <_ 1 ) )
5 1 2 3 4 mpbir3an 
 |-  1 e. ( 0 [,] 1 )