Theorem ltrelnq 11014

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

This proof depends on syntax axioms:   ⊆ wss 3895   ∩ cin 4089   × cxp 5648   <_pQ cltpq 10938  Qcnq 10940   <_Q cltq 10946

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091  df-ltnq 11006

This theorem is used by:  lterpq  11058  ltanq  11059  ltmnq  11060  ltexnq  11063  ltbtwnnq  11066  ltrnq  11067  prcdnq  11081  prnmadd  11085  genpcd  11094  nqpr  11102  1idpr  11117  prlem934  11121  ltexprlem4  11127  prlem936  11135  reclem2pr  11136  reclem3pr  11137  reclem4pr  11138