Theorem ltrelnq 10886

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

Syntax hints:   ∩ cin 3916   ⊆ wss 3917   × cxp 5639   <_pQ cltpq 10810  Qcnq 10812   <_Q cltq 10818

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934  df-ltnq 10878

This theorem is referenced by:  lterpq  10930  ltanq  10931  ltmnq  10932  ltexnq  10935  ltbtwnnq  10938  ltrnq  10939  prcdnq  10953  prnmadd  10957  genpcd  10966  nqpr  10974  1idpr  10989  prlem934  10993  ltexprlem4  10999  prlem936  11007  reclem2pr  11008  reclem3pr  11009  reclem4pr  11010