Theorem ltrelnq 7568

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 7556	. 2 ⊢ <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
2		opabssxp 4795	. 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 4718  (class class class)co 6010  [cec 6691   ·_N cmi 7477   <_N clti 7478   ~_Q ceq 7482  Qcnq 7483   <_Q cltq 7488

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 4726  df-ltnqqs 7556

This theorem is referenced by:  ltanqi  7605  ltmnqi  7606  lt2addnq  7607  lt2mulnq  7608  ltexnqi  7612  ltbtwnnqq  7618  ltbtwnnq  7619  prarloclemarch2  7622  ltrnqi  7624  prcdnql  7687  prcunqu  7688  prnmaxl  7691  prnminu  7692  prloc  7694  prarloclemcalc  7705  genplt2i  7713  genpcdl  7722  genpcuu  7723  genpdisj  7726  addnqprllem  7730  addnqprulem  7731  addlocprlemlt  7734  addlocprlemeq  7736  addlocprlemgt  7737  addlocprlem  7738  nqprdisj  7747  nqprloc  7748  nqprxx  7749  ltnqex  7752  gtnqex  7753  addnqprlemrl  7760  addnqprlemru  7761  addnqprlemfl  7762  addnqprlemfu  7763  appdivnq  7766  prmuloclemcalc  7768  prmuloc  7769  mulnqprlemrl  7776  mulnqprlemru  7777  mulnqprlemfl  7778  mulnqprlemfu  7779  1idprl  7793  1idpru  7794  ltnqpri  7797  ltsopr  7799  ltexprlemopl  7804  ltexprlemopu  7806  ltexprlemdisj  7809  ltexprlemloc  7810  ltexprlemfl  7812  ltexprlemru  7815  recexprlemell  7825  recexprlemelu  7826  recexprlemlol  7829  recexprlemupu  7831  recexprlemdisj  7833  recexprlemloc  7834  recexprlempr  7835  recexprlem1ssl  7836  recexprlem1ssu  7837  recexprlemss1l  7838  recexprlemss1u  7839  cauappcvgprlemm  7848  cauappcvgprlemopl  7849  cauappcvgprlemlol  7850  cauappcvgprlemupu  7852  cauappcvgprlemladdfu  7857  cauappcvgprlemladdfl  7858  caucvgprlemk  7868  caucvgprlemnkj  7869  caucvgprlemnbj  7870  caucvgprlemm  7871  caucvgprlemopl  7872  caucvgprlemlol  7873  caucvgprlemupu  7875  caucvgprlemloc  7878  caucvgprlemladdfu  7880  caucvgprprlemloccalc  7887  caucvgprprlemml  7897  caucvgprprlemopl  7900  caucvgprprlemlol  7901  caucvgprprlemupu  7903  caucvgprprlemloc  7906  suplocexprlemrl  7920  suplocexprlemru  7922