Theorem ltrelnq 10824

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

Syntax hints:   ∩ cin 3897   ⊆ wss 3898   × cxp 5617   <_pQ cltpq 10748  Qcnq 10750   <_Q cltq 10756

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-in 3905  df-ss 3915  df-ltnq 10816

This theorem is referenced by:  lterpq  10868  ltanq  10869  ltmnq  10870  ltexnq  10873  ltbtwnnq  10876  ltrnq  10877  prcdnq  10891  prnmadd  10895  genpcd  10904  nqpr  10912  1idpr  10927  prlem934  10931  ltexprlem4  10937  prlem936  10945  reclem2pr  10946  reclem3pr  10947  reclem4pr  10948