Theorem ltrelnq 7578

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

Syntax hints:   ∧ wa 104   = wceq 1395  ∃wex 1538   ∈ wcel 2200   ⊆ wss 3198  ⟨cop 3670   class class class wbr 4086  {copab 4147   × cxp 4721  (class class class)co 6013  [cec 6695   ·_N cmi 7487   <_N clti 7488   ~_Q ceq 7492  Qcnq 7493   <_Q cltq 7498

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 3204  df-ss 3211  df-opab 4149  df-xp 4729  df-ltnqqs 7566

This theorem is referenced by:  ltanqi  7615  ltmnqi  7616  lt2addnq  7617  lt2mulnq  7618  ltexnqi  7622  ltbtwnnqq  7628  ltbtwnnq  7629  prarloclemarch2  7632  ltrnqi  7634  prcdnql  7697  prcunqu  7698  prnmaxl  7701  prnminu  7702  prloc  7704  prarloclemcalc  7715  genplt2i  7723  genpcdl  7732  genpcuu  7733  genpdisj  7736  addnqprllem  7740  addnqprulem  7741  addlocprlemlt  7744  addlocprlemeq  7746  addlocprlemgt  7747  addlocprlem  7748  nqprdisj  7757  nqprloc  7758  nqprxx  7759  ltnqex  7762  gtnqex  7763  addnqprlemrl  7770  addnqprlemru  7771  addnqprlemfl  7772  addnqprlemfu  7773  appdivnq  7776  prmuloclemcalc  7778  prmuloc  7779  mulnqprlemrl  7786  mulnqprlemru  7787  mulnqprlemfl  7788  mulnqprlemfu  7789  1idprl  7803  1idpru  7804  ltnqpri  7807  ltsopr  7809  ltexprlemopl  7814  ltexprlemopu  7816  ltexprlemdisj  7819  ltexprlemloc  7820  ltexprlemfl  7822  ltexprlemru  7825  recexprlemell  7835  recexprlemelu  7836  recexprlemlol  7839  recexprlemupu  7841  recexprlemdisj  7843  recexprlemloc  7844  recexprlempr  7845  recexprlem1ssl  7846  recexprlem1ssu  7847  recexprlemss1l  7848  recexprlemss1u  7849  cauappcvgprlemm  7858  cauappcvgprlemopl  7859  cauappcvgprlemlol  7860  cauappcvgprlemupu  7862  cauappcvgprlemladdfu  7867  cauappcvgprlemladdfl  7868  caucvgprlemk  7878  caucvgprlemnkj  7879  caucvgprlemnbj  7880  caucvgprlemm  7881  caucvgprlemopl  7882  caucvgprlemlol  7883  caucvgprlemupu  7885  caucvgprlemloc  7888  caucvgprlemladdfu  7890  caucvgprprlemloccalc  7897  caucvgprprlemml  7907  caucvgprprlemopl  7910  caucvgprprlemlol  7911  caucvgprprlemupu  7913  caucvgprprlemloc  7916  suplocexprlemrl  7930  suplocexprlemru  7932