Metamath Proof Explorer

Theorem ex-po

Description: Example for df-po . Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Assertion ex-po 
|- ( < Po RR /\ -. <_ Po RR )

Proof

Step Hyp Ref Expression
1 ltso 
 |-  < Or RR
2 sopo 
 |-  ( < Or RR -> < Po RR )
3 1 2 ax-mp 
 |-  < Po RR
4 0le0 
 |-  0 <_ 0
5 0re 
 |-  0 e. RR
6 poirr 
 |-  ( ( <_ Po RR /\ 0 e. RR ) -> -. 0 <_ 0 )
7 5 6 mpan2 
 |-  ( <_ Po RR -> -. 0 <_ 0 )
8 4 7 mt2 
 |-  -. <_ Po RR
9 3 8 pm3.2i 
 |-  ( < Po RR /\ -. <_ Po RR )