Metamath Proof Explorer

Theorem iirev

Description: Reverse the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion iirev 
|- ( X e. ( 0 [,] 1 ) -> ( 1 - X ) e. ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 resubcl 
 |-  ( ( 1 e. RR /\ X e. RR ) -> ( 1 - X ) e. RR )
3 1 2 mpan 
 |-  ( X e. RR -> ( 1 - X ) e. RR )
4 3 3ad2ant1 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ 1 ) -> ( 1 - X ) e. RR )
5 simp3 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ 1 ) -> X <_ 1 )
6 simp1 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ 1 ) -> X e. RR )
7 subge0 
 |-  ( ( 1 e. RR /\ X e. RR ) -> ( 0 <_ ( 1 - X ) <-> X <_ 1 ) )
8 1 6 7 sylancr 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ 1 ) -> ( 0 <_ ( 1 - X ) <-> X <_ 1 ) )
9 5 8 mpbird 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ 1 ) -> 0 <_ ( 1 - X ) )
10 simp2 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ 1 ) -> 0 <_ X )
11 subge02 
 |-  ( ( 1 e. RR /\ X e. RR ) -> ( 0 <_ X <-> ( 1 - X ) <_ 1 ) )
12 1 6 11 sylancr 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ 1 ) -> ( 0 <_ X <-> ( 1 - X ) <_ 1 ) )
13 10 12 mpbid 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ 1 ) -> ( 1 - X ) <_ 1 )
14 4 9 13 3jca 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ 1 ) -> ( ( 1 - X ) e. RR /\ 0 <_ ( 1 - X ) /\ ( 1 - X ) <_ 1 ) )
15 elicc01 
 |-  ( X e. ( 0 [,] 1 ) <-> ( X e. RR /\ 0 <_ X /\ X <_ 1 ) )
16 elicc01 
 |-  ( ( 1 - X ) e. ( 0 [,] 1 ) <-> ( ( 1 - X ) e. RR /\ 0 <_ ( 1 - X ) /\ ( 1 - X ) <_ 1 ) )
17 14 15 16 3imtr4i 
 |-  ( X e. ( 0 [,] 1 ) -> ( 1 - X ) e. ( 0 [,] 1 ) )