Theorem ltrelnq 7520

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

Syntax hints:   ∧ wa 104   = wceq 1375  ∃wex 1518   ∈ wcel 2180   ⊆ wss 3177  ⟨cop 3649   class class class wbr 4062  {copab 4123   × cxp 4694  (class class class)co 5974  [cec 6648   ·_N cmi 7429   <_N clti 7430   ~_Q ceq 7434  Qcnq 7435   <_Q cltq 7440

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-in 3183  df-ss 3190  df-opab 4125  df-xp 4702  df-ltnqqs 7508

This theorem is referenced by:  ltanqi  7557  ltmnqi  7558  lt2addnq  7559  lt2mulnq  7560  ltexnqi  7564  ltbtwnnqq  7570  ltbtwnnq  7571  prarloclemarch2  7574  ltrnqi  7576  prcdnql  7639  prcunqu  7640  prnmaxl  7643  prnminu  7644  prloc  7646  prarloclemcalc  7657  genplt2i  7665  genpcdl  7674  genpcuu  7675  genpdisj  7678  addnqprllem  7682  addnqprulem  7683  addlocprlemlt  7686  addlocprlemeq  7688  addlocprlemgt  7689  addlocprlem  7690  nqprdisj  7699  nqprloc  7700  nqprxx  7701  ltnqex  7704  gtnqex  7705  addnqprlemrl  7712  addnqprlemru  7713  addnqprlemfl  7714  addnqprlemfu  7715  appdivnq  7718  prmuloclemcalc  7720  prmuloc  7721  mulnqprlemrl  7728  mulnqprlemru  7729  mulnqprlemfl  7730  mulnqprlemfu  7731  1idprl  7745  1idpru  7746  ltnqpri  7749  ltsopr  7751  ltexprlemopl  7756  ltexprlemopu  7758  ltexprlemdisj  7761  ltexprlemloc  7762  ltexprlemfl  7764  ltexprlemru  7767  recexprlemell  7777  recexprlemelu  7778  recexprlemlol  7781  recexprlemupu  7783  recexprlemdisj  7785  recexprlemloc  7786  recexprlempr  7787  recexprlem1ssl  7788  recexprlem1ssu  7789  recexprlemss1l  7790  recexprlemss1u  7791  cauappcvgprlemm  7800  cauappcvgprlemopl  7801  cauappcvgprlemlol  7802  cauappcvgprlemupu  7804  cauappcvgprlemladdfu  7809  cauappcvgprlemladdfl  7810  caucvgprlemk  7820  caucvgprlemnkj  7821  caucvgprlemnbj  7822  caucvgprlemm  7823  caucvgprlemopl  7824  caucvgprlemlol  7825  caucvgprlemupu  7827  caucvgprlemloc  7830  caucvgprlemladdfu  7832  caucvgprprlemloccalc  7839  caucvgprprlemml  7849  caucvgprprlemopl  7852  caucvgprprlemlol  7853  caucvgprprlemupu  7855  caucvgprprlemloc  7858  suplocexprlemrl  7872  suplocexprlemru  7874