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 )