Theorem ltrelnq 7590

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

Syntax hints:   ∧ wa 104   = wceq 1397  ∃wex 1540   ∈ wcel 2201   ⊆ wss 3199  ⟨cop 3673   class class class wbr 4089  {copab 4150   × cxp 4725  (class class class)co 6023  [cec 6705   ·_N cmi 7499   <_N clti 7500   ~_Q ceq 7504  Qcnq 7505   <_Q cltq 7510

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 2212

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-in 3205  df-ss 3212  df-opab 4152  df-xp 4733  df-ltnqqs 7578

This theorem is referenced by:  ltanqi  7627  ltmnqi  7628  lt2addnq  7629  lt2mulnq  7630  ltexnqi  7634  ltbtwnnqq  7640  ltbtwnnq  7641  prarloclemarch2  7644  ltrnqi  7646  prcdnql  7709  prcunqu  7710  prnmaxl  7713  prnminu  7714  prloc  7716  prarloclemcalc  7727  genplt2i  7735  genpcdl  7744  genpcuu  7745  genpdisj  7748  addnqprllem  7752  addnqprulem  7753  addlocprlemlt  7756  addlocprlemeq  7758  addlocprlemgt  7759  addlocprlem  7760  nqprdisj  7769  nqprloc  7770  nqprxx  7771  ltnqex  7774  gtnqex  7775  addnqprlemrl  7782  addnqprlemru  7783  addnqprlemfl  7784  addnqprlemfu  7785  appdivnq  7788  prmuloclemcalc  7790  prmuloc  7791  mulnqprlemrl  7798  mulnqprlemru  7799  mulnqprlemfl  7800  mulnqprlemfu  7801  1idprl  7815  1idpru  7816  ltnqpri  7819  ltsopr  7821  ltexprlemopl  7826  ltexprlemopu  7828  ltexprlemdisj  7831  ltexprlemloc  7832  ltexprlemfl  7834  ltexprlemru  7837  recexprlemell  7847  recexprlemelu  7848  recexprlemlol  7851  recexprlemupu  7853  recexprlemdisj  7855  recexprlemloc  7856  recexprlempr  7857  recexprlem1ssl  7858  recexprlem1ssu  7859  recexprlemss1l  7860  recexprlemss1u  7861  cauappcvgprlemm  7870  cauappcvgprlemopl  7871  cauappcvgprlemlol  7872  cauappcvgprlemupu  7874  cauappcvgprlemladdfu  7879  cauappcvgprlemladdfl  7880  caucvgprlemk  7890  caucvgprlemnkj  7891  caucvgprlemnbj  7892  caucvgprlemm  7893  caucvgprlemopl  7894  caucvgprlemlol  7895  caucvgprlemupu  7897  caucvgprlemloc  7900  caucvgprlemladdfu  7902  caucvgprprlemloccalc  7909  caucvgprprlemml  7919  caucvgprprlemopl  7922  caucvgprprlemlol  7923  caucvgprprlemupu  7925  caucvgprprlemloc  7928  suplocexprlemrl  7942  suplocexprlemru  7944