Theorem ltrelnq 10964

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

Syntax hints:   ∩ cin 3962   ⊆ wss 3963   × cxp 5687   <_pQ cltpq 10888  Qcnq 10890   <_Q cltq 10896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-in 3970  df-ss 3980  df-ltnq 10956

This theorem is referenced by:  lterpq  11008  ltanq  11009  ltmnq  11010  ltexnq  11013  ltbtwnnq  11016  ltrnq  11017  prcdnq  11031  prnmadd  11035  genpcd  11044  nqpr  11052  1idpr  11067  prlem934  11071  ltexprlem4  11077  prlem936  11085  reclem2pr  11086  reclem3pr  11087  reclem4pr  11088