Theorem ltrelnq 7449

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

Syntax hints:   ∧ wa 104   = wceq 1364  ∃wex 1506   ∈ wcel 2167   ⊆ wss 3157  ⟨cop 3626   class class class wbr 4034  {copab 4094   × cxp 4662  (class class class)co 5925  [cec 6599   ·_N cmi 7358   <_N clti 7359   ~_Q ceq 7363  Qcnq 7364   <_Q cltq 7369

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-in 3163  df-ss 3170  df-opab 4096  df-xp 4670  df-ltnqqs 7437

This theorem is referenced by:  ltanqi  7486  ltmnqi  7487  lt2addnq  7488  lt2mulnq  7489  ltexnqi  7493  ltbtwnnqq  7499  ltbtwnnq  7500  prarloclemarch2  7503  ltrnqi  7505  prcdnql  7568  prcunqu  7569  prnmaxl  7572  prnminu  7573  prloc  7575  prarloclemcalc  7586  genplt2i  7594  genpcdl  7603  genpcuu  7604  genpdisj  7607  addnqprllem  7611  addnqprulem  7612  addlocprlemlt  7615  addlocprlemeq  7617  addlocprlemgt  7618  addlocprlem  7619  nqprdisj  7628  nqprloc  7629  nqprxx  7630  ltnqex  7633  gtnqex  7634  addnqprlemrl  7641  addnqprlemru  7642  addnqprlemfl  7643  addnqprlemfu  7644  appdivnq  7647  prmuloclemcalc  7649  prmuloc  7650  mulnqprlemrl  7657  mulnqprlemru  7658  mulnqprlemfl  7659  mulnqprlemfu  7660  1idprl  7674  1idpru  7675  ltnqpri  7678  ltsopr  7680  ltexprlemopl  7685  ltexprlemopu  7687  ltexprlemdisj  7690  ltexprlemloc  7691  ltexprlemfl  7693  ltexprlemru  7696  recexprlemell  7706  recexprlemelu  7707  recexprlemlol  7710  recexprlemupu  7712  recexprlemdisj  7714  recexprlemloc  7715  recexprlempr  7716  recexprlem1ssl  7717  recexprlem1ssu  7718  recexprlemss1l  7719  recexprlemss1u  7720  cauappcvgprlemm  7729  cauappcvgprlemopl  7730  cauappcvgprlemlol  7731  cauappcvgprlemupu  7733  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  caucvgprlemk  7749  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemupu  7756  caucvgprlemloc  7759  caucvgprlemladdfu  7761  caucvgprprlemloccalc  7768  caucvgprprlemml  7778  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemupu  7784  caucvgprprlemloc  7787  suplocexprlemrl  7801  suplocexprlemru  7803