Theorem ltrelpi 10046

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

Assertion

Ref	Expression
ltrelpi	⊢ <N ⊆ (N × N)

Proof of Theorem ltrelpi

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

Syntax hints:   ∩ cin 3790   ⊆ wss 3791   E cep 5265   × cxp 5353  Ncnpi 10001   <_N clti 10004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-v 3399  df-in 3798  df-ss 3805  df-lti 10032

This theorem is referenced by:  ltapi  10060  ltmpi  10061  nlt1pi  10063  indpi  10064  ordpipq  10099  ltsonq  10126  archnq  10137