Theorem ltrelnq 7364

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

Syntax hints:   ∧ wa 104   = wceq 1353  ∃wex 1492   ∈ wcel 2148   ⊆ wss 3130  ⟨cop 3596   class class class wbr 4004  {copab 4064   × cxp 4625  (class class class)co 5875  [cec 6533   ·_N cmi 7273   <_N clti 7274   ~_Q ceq 7278  Qcnq 7279   <_Q cltq 7284

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-in 3136  df-ss 3143  df-opab 4066  df-xp 4633  df-ltnqqs 7352

This theorem is referenced by:  ltanqi  7401  ltmnqi  7402  lt2addnq  7403  lt2mulnq  7404  ltexnqi  7408  ltbtwnnqq  7414  ltbtwnnq  7415  prarloclemarch2  7418  ltrnqi  7420  prcdnql  7483  prcunqu  7484  prnmaxl  7487  prnminu  7488  prloc  7490  prarloclemcalc  7501  genplt2i  7509  genpcdl  7518  genpcuu  7519  genpdisj  7522  addnqprllem  7526  addnqprulem  7527  addlocprlemlt  7530  addlocprlemeq  7532  addlocprlemgt  7533  addlocprlem  7534  nqprdisj  7543  nqprloc  7544  nqprxx  7545  ltnqex  7548  gtnqex  7549  addnqprlemrl  7556  addnqprlemru  7557  addnqprlemfl  7558  addnqprlemfu  7559  appdivnq  7562  prmuloclemcalc  7564  prmuloc  7565  mulnqprlemrl  7572  mulnqprlemru  7573  mulnqprlemfl  7574  mulnqprlemfu  7575  1idprl  7589  1idpru  7590  ltnqpri  7593  ltsopr  7595  ltexprlemopl  7600  ltexprlemopu  7602  ltexprlemdisj  7605  ltexprlemloc  7606  ltexprlemfl  7608  ltexprlemru  7611  recexprlemell  7621  recexprlemelu  7622  recexprlemlol  7625  recexprlemupu  7627  recexprlemdisj  7629  recexprlemloc  7630  recexprlempr  7631  recexprlem1ssl  7632  recexprlem1ssu  7633  recexprlemss1l  7634  recexprlemss1u  7635  cauappcvgprlemm  7644  cauappcvgprlemopl  7645  cauappcvgprlemlol  7646  cauappcvgprlemupu  7648  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  caucvgprlemk  7664  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemlol  7669  caucvgprlemupu  7671  caucvgprlemloc  7674  caucvgprlemladdfu  7676  caucvgprprlemloccalc  7683  caucvgprprlemml  7693  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemupu  7699  caucvgprprlemloc  7702  suplocexprlemrl  7716  suplocexprlemru  7718