This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ltsopi

Description: Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996) (Proof shortened by Mario Carneiro, 10-Jul-2014) (New usage is discouraged.)

Ref Expression
Assertion ltsopi 
|-

Proof

Step Hyp Ref Expression
1 df-ni 
 |-  N. = ( _om \ { (/) } )
2 difss 
 |-  ( _om \ { (/) } ) C_ _om
3 omsson 
 |-  _om C_ On
4 2 3 sstri 
 |-  ( _om \ { (/) } ) C_ On
5 1 4 eqsstri 
 |-  N. C_ On
6 epweon 
 |-  _E We On
7 weso 
 |-  ( _E We On -> _E Or On )
8 6 7 ax-mp 
 |-  _E Or On
9 soss 
 |-  ( N. C_ On -> ( _E Or On -> _E Or N. ) )
10 5 8 9 mp2 
 |-  _E Or N.
11 df-lti 
 |-
12 soeq1 
 |-  (  (  ( _E i^i ( N. X. N. ) ) Or N. ) )
13 11 12 ax-mp 
 |-  (  ( _E i^i ( N. X. N. ) ) Or N. )
14 soinxp 
 |-  ( _E Or N. <-> ( _E i^i ( N. X. N. ) ) Or N. )
15 13 14 bitr4i 
 |-  (  _E Or N. )
16 10 15 mpbir 
 |-