Theorem ltrelnq 7197

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

Syntax hints:   ∧ wa 103   = wceq 1332  ∃wex 1469   ∈ wcel 1481   ⊆ wss 3076  ⟨cop 3535   class class class wbr 3937  {copab 3996   × cxp 4545  (class class class)co 5782  [cec 6435   ·_N cmi 7106   <_N clti 7107   ~_Q ceq 7111  Qcnq 7112   <_Q cltq 7117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-in 3082  df-ss 3089  df-opab 3998  df-xp 4553  df-ltnqqs 7185

This theorem is referenced by:  ltanqi  7234  ltmnqi  7235  lt2addnq  7236  lt2mulnq  7237  ltexnqi  7241  ltbtwnnqq  7247  ltbtwnnq  7248  prarloclemarch2  7251  ltrnqi  7253  prcdnql  7316  prcunqu  7317  prnmaxl  7320  prnminu  7321  prloc  7323  prarloclemcalc  7334  genplt2i  7342  genpcdl  7351  genpcuu  7352  genpdisj  7355  addnqprllem  7359  addnqprulem  7360  addlocprlemlt  7363  addlocprlemeq  7365  addlocprlemgt  7366  addlocprlem  7367  nqprdisj  7376  nqprloc  7377  nqprxx  7378  ltnqex  7381  gtnqex  7382  addnqprlemrl  7389  addnqprlemru  7390  addnqprlemfl  7391  addnqprlemfu  7392  appdivnq  7395  prmuloclemcalc  7397  prmuloc  7398  mulnqprlemrl  7405  mulnqprlemru  7406  mulnqprlemfl  7407  mulnqprlemfu  7408  1idprl  7422  1idpru  7423  ltnqpri  7426  ltsopr  7428  ltexprlemopl  7433  ltexprlemopu  7435  ltexprlemdisj  7438  ltexprlemloc  7439  ltexprlemfl  7441  ltexprlemru  7444  recexprlemell  7454  recexprlemelu  7455  recexprlemlol  7458  recexprlemupu  7460  recexprlemdisj  7462  recexprlemloc  7463  recexprlempr  7464  recexprlem1ssl  7465  recexprlem1ssu  7466  recexprlemss1l  7467  recexprlemss1u  7468  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemupu  7481  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  caucvgprlemk  7497  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemupu  7504  caucvgprlemloc  7507  caucvgprlemladdfu  7509  caucvgprprlemloccalc  7516  caucvgprprlemml  7526  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemupu  7532  caucvgprprlemloc  7535  suplocexprlemrl  7549  suplocexprlemru  7551