Theorem ltrelnq 10348

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

Syntax hints:   ∩ cin 3935   ⊆ wss 3936   × cxp 5553   <_pQ cltpq 10272  Qcnq 10274   <_Q cltq 10280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3943  df-ss 3952  df-ltnq 10340

This theorem is referenced by:  lterpq  10392  ltanq  10393  ltmnq  10394  ltexnq  10397  ltbtwnnq  10400  ltrnq  10401  prcdnq  10415  prnmadd  10419  genpcd  10428  nqpr  10436  1idpr  10451  prlem934  10455  ltexprlem4  10461  prlem936  10469  reclem2pr  10470  reclem3pr  10471  reclem4pr  10472