Theorem ltrelnq 10992

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

This proof depends on syntax axioms:   ∩ cin 3898   ⊆ wss 3899   × cxp 5649   <_pQ cltpq 10916  Qcnq 10918   <_Q cltq 10924

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-in 3906  df-ss 3916  df-ltnq 10984

This theorem is used by:  lterpq  11036  ltanq  11037  ltmnq  11038  ltexnq  11041  ltbtwnnq  11044  ltrnq  11045  prcdnq  11059  prnmadd  11063  genpcd  11072  nqpr  11080  1idpr  11095  prlem934  11099  ltexprlem4  11105  prlem936  11113  reclem2pr  11114  reclem3pr  11115  reclem4pr  11116