Theorem ltrelnq 7585

Description: Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.)

Assertion

Ref	Expression
ltrelnq	⊢ <Q ⊆ (Q × Q)

Proof of Theorem ltrelnq

Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ltnqqs 7573	. 2 ⊢ <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
2		opabssxp 4800	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))} ⊆ (Q × Q)
3	1, 2	eqsstri 3259	1 ⊢ <Q ⊆ (Q × Q)

Syntax hints:   ∧ wa 104   = wceq 1397  ∃wex 1540   ∈ wcel 2202   ⊆ wss 3200  ⟨cop 3672   class class class wbr 4088  {copab 4149   × cxp 4723  (class class class)co 6018  [cec 6700   ·_N cmi 7494   <_N clti 7495   ~_Q ceq 7499  Qcnq 7500   <_Q cltq 7505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-in 3206  df-ss 3213  df-opab 4151  df-xp 4731  df-ltnqqs 7573

This theorem is referenced by:  ltanqi  7622  ltmnqi  7623  lt2addnq  7624  lt2mulnq  7625  ltexnqi  7629  ltbtwnnqq  7635  ltbtwnnq  7636  prarloclemarch2  7639  ltrnqi  7641  prcdnql  7704  prcunqu  7705  prnmaxl  7708  prnminu  7709  prloc  7711  prarloclemcalc  7722  genplt2i  7730  genpcdl  7739  genpcuu  7740  genpdisj  7743  addnqprllem  7747  addnqprulem  7748  addlocprlemlt  7751  addlocprlemeq  7753  addlocprlemgt  7754  addlocprlem  7755  nqprdisj  7764  nqprloc  7765  nqprxx  7766  ltnqex  7769  gtnqex  7770  addnqprlemrl  7777  addnqprlemru  7778  addnqprlemfl  7779  addnqprlemfu  7780  appdivnq  7783  prmuloclemcalc  7785  prmuloc  7786  mulnqprlemrl  7793  mulnqprlemru  7794  mulnqprlemfl  7795  mulnqprlemfu  7796  1idprl  7810  1idpru  7811  ltnqpri  7814  ltsopr  7816  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemfl  7829  ltexprlemru  7832  recexprlemell  7842  recexprlemelu  7843  recexprlemlol  7846  recexprlemupu  7848  recexprlemdisj  7850  recexprlemloc  7851  recexprlempr  7852  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1l  7855  recexprlemss1u  7856  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemupu  7869  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  caucvgprlemk  7885  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemupu  7892  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprprlemloccalc  7904  caucvgprprlemml  7914  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemupu  7920  caucvgprprlemloc  7923  suplocexprlemrl  7937  suplocexprlemru  7939