Theorem ltrelnq 7560

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 7548	. 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 6007  [cec 6686   ·_N cmi 7469   <_N clti 7470   ~_Q ceq 7474  Qcnq 7475   <_Q cltq 7480

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 7548

This theorem is referenced by:  ltanqi  7597  ltmnqi  7598  lt2addnq  7599  lt2mulnq  7600  ltexnqi  7604  ltbtwnnqq  7610  ltbtwnnq  7611  prarloclemarch2  7614  ltrnqi  7616  prcdnql  7679  prcunqu  7680  prnmaxl  7683  prnminu  7684  prloc  7686  prarloclemcalc  7697  genplt2i  7705  genpcdl  7714  genpcuu  7715  genpdisj  7718  addnqprllem  7722  addnqprulem  7723  addlocprlemlt  7726  addlocprlemeq  7728  addlocprlemgt  7729  addlocprlem  7730  nqprdisj  7739  nqprloc  7740  nqprxx  7741  ltnqex  7744  gtnqex  7745  addnqprlemrl  7752  addnqprlemru  7753  addnqprlemfl  7754  addnqprlemfu  7755  appdivnq  7758  prmuloclemcalc  7760  prmuloc  7761  mulnqprlemrl  7768  mulnqprlemru  7769  mulnqprlemfl  7770  mulnqprlemfu  7771  1idprl  7785  1idpru  7786  ltnqpri  7789  ltsopr  7791  ltexprlemopl  7796  ltexprlemopu  7798  ltexprlemdisj  7801  ltexprlemloc  7802  ltexprlemfl  7804  ltexprlemru  7807  recexprlemell  7817  recexprlemelu  7818  recexprlemlol  7821  recexprlemupu  7823  recexprlemdisj  7825  recexprlemloc  7826  recexprlempr  7827  recexprlem1ssl  7828  recexprlem1ssu  7829  recexprlemss1l  7830  recexprlemss1u  7831  cauappcvgprlemm  7840  cauappcvgprlemopl  7841  cauappcvgprlemlol  7842  cauappcvgprlemupu  7844  cauappcvgprlemladdfu  7849  cauappcvgprlemladdfl  7850  caucvgprlemk  7860  caucvgprlemnkj  7861  caucvgprlemnbj  7862  caucvgprlemm  7863  caucvgprlemopl  7864  caucvgprlemlol  7865  caucvgprlemupu  7867  caucvgprlemloc  7870  caucvgprlemladdfu  7872  caucvgprprlemloccalc  7879  caucvgprprlemml  7889  caucvgprprlemopl  7892  caucvgprprlemlol  7893  caucvgprprlemupu  7895  caucvgprprlemloc  7898  suplocexprlemrl  7912  suplocexprlemru  7914