Theorem ltrelnq 10967

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

Syntax hints:   ∩ cin 3949   ⊆ wss 3950   × cxp 5682   <_pQ cltpq 10891  Qcnq 10893   <_Q cltq 10899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-in 3957  df-ss 3967  df-ltnq 10959

This theorem is referenced by:  lterpq  11011  ltanq  11012  ltmnq  11013  ltexnq  11016  ltbtwnnq  11019  ltrnq  11020  prcdnq  11034  prnmadd  11038  genpcd  11047  nqpr  11055  1idpr  11070  prlem934  11074  ltexprlem4  11080  prlem936  11088  reclem2pr  11089  reclem3pr  11090  reclem4pr  11091