Theorem ltrelnq 10814

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

Syntax hints:   ∩ cin 3901   ⊆ wss 3902   × cxp 5614   <_pQ cltpq 10738  Qcnq 10740   <_Q cltq 10746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3909  df-ss 3919  df-ltnq 10806

This theorem is referenced by:  lterpq  10858  ltanq  10859  ltmnq  10860  ltexnq  10863  ltbtwnnq  10866  ltrnq  10867  prcdnq  10881  prnmadd  10885  genpcd  10894  nqpr  10902  1idpr  10917  prlem934  10921  ltexprlem4  10927  prlem936  10935  reclem2pr  10936  reclem3pr  10937  reclem4pr  10938