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

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 <N ⊆ ( N × N )

Proof

Step Hyp Ref Expression
1 df-lti ⊢ <N = ( E ∩ ( N × N ) )
2 inss2 ⊢ ( E ∩ ( N × N ) ) ⊆ ( N × N )
3 1 2 eqsstri ⊢ <N ⊆ ( N × N )