Theorem ltrelnq 10083

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

Syntax hints:   ∩ cin 3791   ⊆ wss 3792   × cxp 5353   <_pQ cltpq 10007  Qcnq 10009   <_Q cltq 10015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-in 3799  df-ss 3806  df-ltnq 10075

This theorem is referenced by:  lterpq  10127  ltanq  10128  ltmnq  10129  ltexnq  10132  ltbtwnnq  10135  ltrnq  10136  prcdnq  10150  prnmadd  10154  genpcd  10163  nqpr  10171  1idpr  10186  prlem934  10190  ltexprlem4  10196  prlem936  10204  reclem2pr  10205  reclem3pr  10206  reclem4pr  10207