Theorem ltrelnq 10844

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

Syntax hints:   ∩ cin 3884   ⊆ wss 3885   × cxp 5619   <_pQ cltpq 10768  Qcnq 10770   <_Q cltq 10776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-in 3892  df-ss 3902  df-ltnq 10836

This theorem is referenced by:  lterpq  10888  ltanq  10889  ltmnq  10890  ltexnq  10893  ltbtwnnq  10896  ltrnq  10897  prcdnq  10911  prnmadd  10915  genpcd  10924  nqpr  10932  1idpr  10947  prlem934  10951  ltexprlem4  10957  prlem936  10965  reclem2pr  10966  reclem3pr  10967  reclem4pr  10968