Theorem ltrelnq 7021

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

Syntax hints:   ∧ wa 103   = wceq 1296  ∃wex 1433   ∈ wcel 1445   ⊆ wss 3013  ⟨cop 3469   class class class wbr 3867  {copab 3920   × cxp 4465  (class class class)co 5690  [cec 6330   ·_N cmi 6930   <_N clti 6931   ~_Q ceq 6935  Qcnq 6936   <_Q cltq 6941

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-in 3019  df-ss 3026  df-opab 3922  df-xp 4473  df-ltnqqs 7009

This theorem is referenced by:  ltanqi  7058  ltmnqi  7059  lt2addnq  7060  lt2mulnq  7061  ltexnqi  7065  ltbtwnnqq  7071  ltbtwnnq  7072  prarloclemarch2  7075  ltrnqi  7077  prcdnql  7140  prcunqu  7141  prnmaxl  7144  prnminu  7145  prloc  7147  prarloclemcalc  7158  genplt2i  7166  genpcdl  7175  genpcuu  7176  genpdisj  7179  addnqprllem  7183  addnqprulem  7184  addlocprlemlt  7187  addlocprlemeq  7189  addlocprlemgt  7190  addlocprlem  7191  nqprdisj  7200  nqprloc  7201  nqprxx  7202  ltnqex  7205  gtnqex  7206  addnqprlemrl  7213  addnqprlemru  7214  addnqprlemfl  7215  addnqprlemfu  7216  appdivnq  7219  prmuloclemcalc  7221  prmuloc  7222  mulnqprlemrl  7229  mulnqprlemru  7230  mulnqprlemfl  7231  mulnqprlemfu  7232  1idprl  7246  1idpru  7247  ltnqpri  7250  ltsopr  7252  ltexprlemopl  7257  ltexprlemopu  7259  ltexprlemdisj  7262  ltexprlemloc  7263  ltexprlemfl  7265  ltexprlemru  7268  recexprlemell  7278  recexprlemelu  7279  recexprlemlol  7282  recexprlemupu  7284  recexprlemdisj  7286  recexprlemloc  7287  recexprlempr  7288  recexprlem1ssl  7289  recexprlem1ssu  7290  recexprlemss1l  7291  recexprlemss1u  7292  cauappcvgprlemm  7301  cauappcvgprlemopl  7302  cauappcvgprlemlol  7303  cauappcvgprlemupu  7305  cauappcvgprlemladdfu  7310  cauappcvgprlemladdfl  7311  caucvgprlemk  7321  caucvgprlemnkj  7322  caucvgprlemnbj  7323  caucvgprlemm  7324  caucvgprlemopl  7325  caucvgprlemlol  7326  caucvgprlemupu  7328  caucvgprlemloc  7331  caucvgprlemladdfu  7333  caucvgprprlemloccalc  7340  caucvgprprlemml  7350  caucvgprprlemopl  7353  caucvgprprlemlol  7354  caucvgprprlemupu  7356  caucvgprprlemloc  7359