Metamath Proof Explorer

Theorem ltrelpi

Description: Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion ltrelpi 
|-

Proof

Step Hyp Ref Expression
1 df-lti 
 |-
2 inss2 
 |-  ( _E i^i ( N. X. N. ) ) C_ ( N. X. N. )
3 1 2 eqsstri 
 |-