Theorem ltrelnq 10929

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

This proof depends on syntax axioms:   ∩ cin 3907   ⊆ wss 3908   × cxp 5664   <_pQ cltpq 10853  Qcnq 10855   <_Q cltq 10861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-in 3915  df-ss 3925  df-ltnq 10921

This theorem is used by:  lterpq  10973  ltanq  10974  ltmnq  10975  ltexnq  10978  ltbtwnnq  10981  ltrnq  10982  prcdnq  10996  prnmadd  11000  genpcd  11009  nqpr  11017  1idpr  11032  prlem934  11036  ltexprlem4  11042  prlem936  11050  reclem2pr  11051  reclem3pr  11052  reclem4pr  11053