Theorem ltrelnq 10350

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

Syntax hints:   ∩ cin 3937   ⊆ wss 3938   × cxp 5555   <_pQ cltpq 10274  Qcnq 10276   <_Q cltq 10282

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-in 3945  df-ss 3954  df-ltnq 10342

This theorem is referenced by:  lterpq  10394  ltanq  10395  ltmnq  10396  ltexnq  10399  ltbtwnnq  10402  ltrnq  10403  prcdnq  10417  prnmadd  10421  genpcd  10430  nqpr  10438  1idpr  10453  prlem934  10457  ltexprlem4  10463  prlem936  10471  reclem2pr  10472  reclem3pr  10473  reclem4pr  10474