Theorem ltrelnq 10682

Description: Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.)

Assertion

Ref	Expression
ltrelnq	⊢ <Q ⊆ (Q × Q)

Proof of Theorem ltrelnq

Step	Hyp	Ref	Expression
1		df-ltnq 10674	. 2 ⊢ <Q = ( <pQ ∩ (Q × Q))
2		inss2 4163	. 2 ⊢ ( <pQ ∩ (Q × Q)) ⊆ (Q × Q)
3	1, 2	eqsstri 3955	1 ⊢ <Q ⊆ (Q × Q)

Syntax hints:   ∩ cin 3886   ⊆ wss 3887   × cxp 5587   <_pQ cltpq 10606  Qcnq 10608   <_Q cltq 10614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-ltnq 10674

This theorem is referenced by:  lterpq  10726  ltanq  10727  ltmnq  10728  ltexnq  10731  ltbtwnnq  10734  ltrnq  10735  prcdnq  10749  prnmadd  10753  genpcd  10762  nqpr  10770  1idpr  10785  prlem934  10789  ltexprlem4  10795  prlem936  10803  reclem2pr  10804  reclem3pr  10805  reclem4pr  10806