Theorem ltrelnq 10839

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 10831	. 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 3904   ⊆ wss 3905   × cxp 5621   <_pQ cltpq 10763  Qcnq 10765   <_Q cltq 10771

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 3397  df-v 3440  df-in 3912  df-ss 3922  df-ltnq 10831

This theorem is referenced by:  lterpq  10883  ltanq  10884  ltmnq  10885  ltexnq  10888  ltbtwnnq  10891  ltrnq  10892  prcdnq  10906  prnmadd  10910  genpcd  10919  nqpr  10927  1idpr  10942  prlem934  10946  ltexprlem4  10952  prlem936  10960  reclem2pr  10961  reclem3pr  10962  reclem4pr  10963