Theorem ltrelnq 10847

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

Syntax hints:   ∩ cin 3889   ⊆ wss 3890   × cxp 5623   <_pQ cltpq 10771  Qcnq 10773   <_Q cltq 10779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-in 3897  df-ss 3907  df-ltnq 10839

This theorem is referenced by:  lterpq  10891  ltanq  10892  ltmnq  10893  ltexnq  10896  ltbtwnnq  10899  ltrnq  10900  prcdnq  10914  prnmadd  10918  genpcd  10927  nqpr  10935  1idpr  10950  prlem934  10954  ltexprlem4  10960  prlem936  10968  reclem2pr  10969  reclem3pr  10970  reclem4pr  10971