Theorem ltrelnq 10912

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 10904	. 2 ⊢ <Q = ( <pQ ∩ (Q × Q))
2		inss2 4191	. 2 ⊢ ( <pQ ∩ (Q × Q)) ⊆ (Q × Q)
3	1, 2	eqsstri 3984	1 ⊢ <Q ⊆ (Q × Q)

Syntax hints:   ∩ cin 3905   ⊆ wss 3906   × cxp 5661   <_pQ cltpq 10836  Qcnq 10838   <_Q cltq 10844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3913  df-ss 3923  df-ltnq 10904

This theorem is referenced by:  lterpq  10956  ltanq  10957  ltmnq  10958  ltexnq  10961  ltbtwnnq  10964  ltrnq  10965  prcdnq  10979  prnmadd  10983  genpcd  10992  nqpr  11000  1idpr  11015  prlem934  11019  ltexprlem4  11025  prlem936  11033  reclem2pr  11034  reclem3pr  11035  reclem4pr  11036