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
 |-