Theorem ltrelnq 10945

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

Syntax hints:   ∩ cin 3930   ⊆ wss 3931   × cxp 5657   <_pQ cltpq 10869  Qcnq 10871   <_Q cltq 10877

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-in 3938  df-ss 3948  df-ltnq 10937

This theorem is referenced by:  lterpq  10989  ltanq  10990  ltmnq  10991  ltexnq  10994  ltbtwnnq  10997  ltrnq  10998  prcdnq  11012  prnmadd  11016  genpcd  11025  nqpr  11033  1idpr  11048  prlem934  11052  ltexprlem4  11058  prlem936  11066  reclem2pr  11067  reclem3pr  11068  reclem4pr  11069