Theorem ltrelnq 10881

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

Syntax hints:   ∩ cin 3903   ⊆ wss 3904   × cxp 5643   <_pQ cltpq 10805  Qcnq 10807   <_Q cltq 10813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-in 3911  df-ss 3921  df-ltnq 10873

This theorem is referenced by:  lterpq  10925  ltanq  10926  ltmnq  10927  ltexnq  10930  ltbtwnnq  10933  ltrnq  10934  prcdnq  10948  prnmadd  10952  genpcd  10961  nqpr  10969  1idpr  10984  prlem934  10988  ltexprlem4  10994  prlem936  11002  reclem2pr  11003  reclem3pr  11004  reclem4pr  11005