Theorem ltrelnq 7485

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 7473	. 2 ⊢ <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
2		opabssxp 4753	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))} ⊆ (Q × Q)
3	1, 2	eqsstri 3226	1 ⊢ <Q ⊆ (Q × Q)

Syntax hints:   ∧ wa 104   = wceq 1373  ∃wex 1516   ∈ wcel 2177   ⊆ wss 3167  ⟨cop 3637   class class class wbr 4047  {copab 4108   × cxp 4677  (class class class)co 5951  [cec 6625   ·_N cmi 7394   <_N clti 7395   ~_Q ceq 7399  Qcnq 7400   <_Q cltq 7405

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-in 3173  df-ss 3180  df-opab 4110  df-xp 4685  df-ltnqqs 7473

This theorem is referenced by:  ltanqi  7522  ltmnqi  7523  lt2addnq  7524  lt2mulnq  7525  ltexnqi  7529  ltbtwnnqq  7535  ltbtwnnq  7536  prarloclemarch2  7539  ltrnqi  7541  prcdnql  7604  prcunqu  7605  prnmaxl  7608  prnminu  7609  prloc  7611  prarloclemcalc  7622  genplt2i  7630  genpcdl  7639  genpcuu  7640  genpdisj  7643  addnqprllem  7647  addnqprulem  7648  addlocprlemlt  7651  addlocprlemeq  7653  addlocprlemgt  7654  addlocprlem  7655  nqprdisj  7664  nqprloc  7665  nqprxx  7666  ltnqex  7669  gtnqex  7670  addnqprlemrl  7677  addnqprlemru  7678  addnqprlemfl  7679  addnqprlemfu  7680  appdivnq  7683  prmuloclemcalc  7685  prmuloc  7686  mulnqprlemrl  7693  mulnqprlemru  7694  mulnqprlemfl  7695  mulnqprlemfu  7696  1idprl  7710  1idpru  7711  ltnqpri  7714  ltsopr  7716  ltexprlemopl  7721  ltexprlemopu  7723  ltexprlemdisj  7726  ltexprlemloc  7727  ltexprlemfl  7729  ltexprlemru  7732  recexprlemell  7742  recexprlemelu  7743  recexprlemlol  7746  recexprlemupu  7748  recexprlemdisj  7750  recexprlemloc  7751  recexprlempr  7752  recexprlem1ssl  7753  recexprlem1ssu  7754  recexprlemss1l  7755  recexprlemss1u  7756  cauappcvgprlemm  7765  cauappcvgprlemopl  7766  cauappcvgprlemlol  7767  cauappcvgprlemupu  7769  cauappcvgprlemladdfu  7774  cauappcvgprlemladdfl  7775  caucvgprlemk  7785  caucvgprlemnkj  7786  caucvgprlemnbj  7787  caucvgprlemm  7788  caucvgprlemopl  7789  caucvgprlemlol  7790  caucvgprlemupu  7792  caucvgprlemloc  7795  caucvgprlemladdfu  7797  caucvgprprlemloccalc  7804  caucvgprprlemml  7814  caucvgprprlemopl  7817  caucvgprprlemlol  7818  caucvgprprlemupu  7820  caucvgprprlemloc  7823  suplocexprlemrl  7837  suplocexprlemru  7839