Theorem ltrelnq 10939

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

This proof depends on syntax axioms:   ∩ cin 3901   ⊆ wss 3902   × cxp 5657   <_pQ cltpq 10863  Qcnq 10865   <_Q cltq 10871

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-in 3909  df-ss 3919  df-ltnq 10931

This theorem is used by:  lterpq  10983  ltanq  10984  ltmnq  10985  ltexnq  10988  ltbtwnnq  10991  ltrnq  10992  prcdnq  11006  prnmadd  11010  genpcd  11019  nqpr  11027  1idpr  11042  prlem934  11046  ltexprlem4  11052  prlem936  11060  reclem2pr  11061  reclem3pr  11062  reclem4pr  11063