Theorem ltrelnq 10337

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

Syntax hints:   ∩ cin 3880   ⊆ wss 3881   × cxp 5517   <_pQ cltpq 10261  Qcnq 10263   <_Q cltq 10269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-ltnq 10329

This theorem is referenced by:  lterpq  10381  ltanq  10382  ltmnq  10383  ltexnq  10386  ltbtwnnq  10389  ltrnq  10390  prcdnq  10404  prnmadd  10408  genpcd  10417  nqpr  10425  1idpr  10440  prlem934  10444  ltexprlem4  10450  prlem936  10458  reclem2pr  10459  reclem3pr  10460  reclem4pr  10461