Theorem ltrelnq 7425

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

Syntax hints:   ∧ wa 104   = wceq 1364  ∃wex 1503   ∈ wcel 2164   ⊆ wss 3153  ⟨cop 3621   class class class wbr 4029  {copab 4089   × cxp 4657  (class class class)co 5918  [cec 6585   ·_N cmi 7334   <_N clti 7335   ~_Q ceq 7339  Qcnq 7340   <_Q cltq 7345

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-in 3159  df-ss 3166  df-opab 4091  df-xp 4665  df-ltnqqs 7413

This theorem is referenced by:  ltanqi  7462  ltmnqi  7463  lt2addnq  7464  lt2mulnq  7465  ltexnqi  7469  ltbtwnnqq  7475  ltbtwnnq  7476  prarloclemarch2  7479  ltrnqi  7481  prcdnql  7544  prcunqu  7545  prnmaxl  7548  prnminu  7549  prloc  7551  prarloclemcalc  7562  genplt2i  7570  genpcdl  7579  genpcuu  7580  genpdisj  7583  addnqprllem  7587  addnqprulem  7588  addlocprlemlt  7591  addlocprlemeq  7593  addlocprlemgt  7594  addlocprlem  7595  nqprdisj  7604  nqprloc  7605  nqprxx  7606  ltnqex  7609  gtnqex  7610  addnqprlemrl  7617  addnqprlemru  7618  addnqprlemfl  7619  addnqprlemfu  7620  appdivnq  7623  prmuloclemcalc  7625  prmuloc  7626  mulnqprlemrl  7633  mulnqprlemru  7634  mulnqprlemfl  7635  mulnqprlemfu  7636  1idprl  7650  1idpru  7651  ltnqpri  7654  ltsopr  7656  ltexprlemopl  7661  ltexprlemopu  7663  ltexprlemdisj  7666  ltexprlemloc  7667  ltexprlemfl  7669  ltexprlemru  7672  recexprlemell  7682  recexprlemelu  7683  recexprlemlol  7686  recexprlemupu  7688  recexprlemdisj  7690  recexprlemloc  7691  recexprlempr  7692  recexprlem1ssl  7693  recexprlem1ssu  7694  recexprlemss1l  7695  recexprlemss1u  7696  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemupu  7709  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  caucvgprlemk  7725  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemupu  7732  caucvgprlemloc  7735  caucvgprlemladdfu  7737  caucvgprprlemloccalc  7744  caucvgprprlemml  7754  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemupu  7760  caucvgprprlemloc  7763  suplocexprlemrl  7777  suplocexprlemru  7779