Theorem ltrelnq 7552

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

Syntax hints:   ∧ wa 104   = wceq 1395  ∃wex 1538   ∈ wcel 2200   ⊆ wss 3197  ⟨cop 3669   class class class wbr 4083  {copab 4144   × cxp 4717  (class class class)co 6001  [cec 6678   ·_N cmi 7461   <_N clti 7462   ~_Q ceq 7466  Qcnq 7467   <_Q cltq 7472

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-in 3203  df-ss 3210  df-opab 4146  df-xp 4725  df-ltnqqs 7540

This theorem is referenced by:  ltanqi  7589  ltmnqi  7590  lt2addnq  7591  lt2mulnq  7592  ltexnqi  7596  ltbtwnnqq  7602  ltbtwnnq  7603  prarloclemarch2  7606  ltrnqi  7608  prcdnql  7671  prcunqu  7672  prnmaxl  7675  prnminu  7676  prloc  7678  prarloclemcalc  7689  genplt2i  7697  genpcdl  7706  genpcuu  7707  genpdisj  7710  addnqprllem  7714  addnqprulem  7715  addlocprlemlt  7718  addlocprlemeq  7720  addlocprlemgt  7721  addlocprlem  7722  nqprdisj  7731  nqprloc  7732  nqprxx  7733  ltnqex  7736  gtnqex  7737  addnqprlemrl  7744  addnqprlemru  7745  addnqprlemfl  7746  addnqprlemfu  7747  appdivnq  7750  prmuloclemcalc  7752  prmuloc  7753  mulnqprlemrl  7760  mulnqprlemru  7761  mulnqprlemfl  7762  mulnqprlemfu  7763  1idprl  7777  1idpru  7778  ltnqpri  7781  ltsopr  7783  ltexprlemopl  7788  ltexprlemopu  7790  ltexprlemdisj  7793  ltexprlemloc  7794  ltexprlemfl  7796  ltexprlemru  7799  recexprlemell  7809  recexprlemelu  7810  recexprlemlol  7813  recexprlemupu  7815  recexprlemdisj  7817  recexprlemloc  7818  recexprlempr  7819  recexprlem1ssl  7820  recexprlem1ssu  7821  recexprlemss1l  7822  recexprlemss1u  7823  cauappcvgprlemm  7832  cauappcvgprlemopl  7833  cauappcvgprlemlol  7834  cauappcvgprlemupu  7836  cauappcvgprlemladdfu  7841  cauappcvgprlemladdfl  7842  caucvgprlemk  7852  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprlemm  7855  caucvgprlemopl  7856  caucvgprlemlol  7857  caucvgprlemupu  7859  caucvgprlemloc  7862  caucvgprlemladdfu  7864  caucvgprprlemloccalc  7871  caucvgprprlemml  7881  caucvgprprlemopl  7884  caucvgprprlemlol  7885  caucvgprprlemupu  7887  caucvgprprlemloc  7890  suplocexprlemrl  7904  suplocexprlemru  7906