MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addnqf Structured version   Visualization version   GIF version

Theorem addnqf 10589
Description: Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.)
Assertion
Ref Expression
addnqf +Q :(Q × Q)⟶Q

Proof of Theorem addnqf
StepHypRef Expression
1 nqerf 10571 . . . 4 [Q]:(N × N)⟶Q
2 addpqf 10585 . . . 4 +pQ :((N × N) × (N × N))⟶(N × N)
3 fco 6590 . . . 4 (([Q]:(N × N)⟶Q ∧ +pQ :((N × N) × (N × N))⟶(N × N)) → ([Q] ∘ +pQ ):((N × N) × (N × N))⟶Q)
41, 2, 3mp2an 692 . . 3 ([Q] ∘ +pQ ):((N × N) × (N × N))⟶Q
5 elpqn 10566 . . . . 5 (𝑥Q𝑥 ∈ (N × N))
65ssriv 3921 . . . 4 Q ⊆ (N × N)
7 xpss12 5583 . . . 4 ((Q ⊆ (N × N) ∧ Q ⊆ (N × N)) → (Q × Q) ⊆ ((N × N) × (N × N)))
86, 6, 7mp2an 692 . . 3 (Q × Q) ⊆ ((N × N) × (N × N))
9 fssres 6606 . . 3 ((([Q] ∘ +pQ ):((N × N) × (N × N))⟶Q ∧ (Q × Q) ⊆ ((N × N) × (N × N))) → (([Q] ∘ +pQ ) ↾ (Q × Q)):(Q × Q)⟶Q)
104, 8, 9mp2an 692 . 2 (([Q] ∘ +pQ ) ↾ (Q × Q)):(Q × Q)⟶Q
11 df-plq 10555 . . 3 +Q = (([Q] ∘ +pQ ) ↾ (Q × Q))
1211feq1i 6557 . 2 ( +Q :(Q × Q)⟶Q ↔ (([Q] ∘ +pQ ) ↾ (Q × Q)):(Q × Q)⟶Q)
1310, 12mpbir 234 1 +Q :(Q × Q)⟶Q
Colors of variables: wff setvar class
Syntax hints:  wss 3882   × cxp 5566  cres 5570  ccom 5572  wf 6396  Ncnpi 10485   +pQ cplpq 10489  Qcnq 10493  [Q]cerq 10495   +Q cplq 10496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pr 5338  ax-un 7544
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3711  df-csb 3828  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4836  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-tr 5178  df-id 5471  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-we 5528  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-pred 6178  df-ord 6236  df-on 6237  df-lim 6238  df-suc 6239  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-ov 7237  df-oprab 7238  df-mpo 7239  df-om 7666  df-1st 7782  df-2nd 7783  df-wrecs 8070  df-recs 8131  df-rdg 8169  df-1o 8225  df-oadd 8229  df-omul 8230  df-er 8414  df-ni 10513  df-pli 10514  df-mi 10515  df-lti 10516  df-plpq 10549  df-enq 10552  df-nq 10553  df-erq 10554  df-plq 10555  df-1nq 10557
This theorem is referenced by:  addcomnq  10592  adderpq  10597  addassnq  10599  distrnq  10602  ltanq  10612  ltexnq  10616  nsmallnq  10618  ltbtwnnq  10619  prlem934  10674  ltaddpr  10675  ltexprlem2  10678  ltexprlem3  10679  ltexprlem4  10680  ltexprlem6  10682  ltexprlem7  10683  prlem936  10688
  Copyright terms: Public domain W3C validator