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	$$⊢{<}_{𝑵}\subseteq 𝑵\times 𝑵$$

Proof

Step	Hyp	Ref	Expression
1		df-lti	$$⊢{<}_{𝑵}=\mathrm{E}\cap \left(𝑵\times 𝑵\right)$$
2		inss2	$$⊢\mathrm{E}\cap \left(𝑵\times 𝑵\right)\subseteq 𝑵\times 𝑵$$
3	1 2	eqsstri	$$⊢{<}_{𝑵}\subseteq 𝑵\times 𝑵$$