Theorem ltrelnq 10613

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

Syntax hints:   ∩ cin 3882   ⊆ wss 3883   × cxp 5578   <_pQ cltpq 10537  Qcnq 10539   <_Q cltq 10545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-ltnq 10605

This theorem is referenced by:  lterpq  10657  ltanq  10658  ltmnq  10659  ltexnq  10662  ltbtwnnq  10665  ltrnq  10666  prcdnq  10680  prnmadd  10684  genpcd  10693  nqpr  10701  1idpr  10716  prlem934  10720  ltexprlem4  10726  prlem936  10734  reclem2pr  10735  reclem3pr  10736  reclem4pr  10737