Theorem ltrelnq 10840

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

Syntax hints:   ∩ cin 3889   ⊆ wss 3890   × cxp 5622   <_pQ cltpq 10764  Qcnq 10766   <_Q cltq 10772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907  df-ltnq 10832

This theorem is referenced by:  lterpq  10884  ltanq  10885  ltmnq  10886  ltexnq  10889  ltbtwnnq  10892  ltrnq  10893  prcdnq  10907  prnmadd  10911  genpcd  10920  nqpr  10928  1idpr  10943  prlem934  10947  ltexprlem4  10953  prlem936  10961  reclem2pr  10962  reclem3pr  10963  reclem4pr  10964