Theorem ltrelnq 10683

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

Syntax hints:   ∩ cin 3891   ⊆ wss 3892   × cxp 5588   <_pQ cltpq 10607  Qcnq 10609   <_Q cltq 10615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-in 3899  df-ss 3909  df-ltnq 10675

This theorem is referenced by:  lterpq  10727  ltanq  10728  ltmnq  10729  ltexnq  10732  ltbtwnnq  10735  ltrnq  10736  prcdnq  10750  prnmadd  10754  genpcd  10763  nqpr  10771  1idpr  10786  prlem934  10790  ltexprlem4  10796  prlem936  10804  reclem2pr  10805  reclem3pr  10806  reclem4pr  10807