Theorem ltrelnq 10879

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

Syntax hints:   ∩ cin 3913   ⊆ wss 3914   × cxp 5636   <_pQ cltpq 10803  Qcnq 10805   <_Q cltq 10811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931  df-ltnq 10871

This theorem is referenced by:  lterpq  10923  ltanq  10924  ltmnq  10925  ltexnq  10928  ltbtwnnq  10931  ltrnq  10932  prcdnq  10946  prnmadd  10950  genpcd  10959  nqpr  10967  1idpr  10982  prlem934  10986  ltexprlem4  10992  prlem936  11000  reclem2pr  11001  reclem3pr  11002  reclem4pr  11003