Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > addnqf | Structured version Visualization version GIF version |
Description: Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |
Ref | Expression |
---|---|
addnqf | ⊢ +Q :(Q × Q)⟶Q |
Step | Hyp | Ref | 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) | |
4 | 1, 2, 3 | mp2an 692 | . . 3 ⊢ ([Q] ∘ +pQ ):((N × N) × (N × N))⟶Q |
5 | elpqn 10566 | . . . . 5 ⊢ (𝑥 ∈ Q → 𝑥 ∈ (N × N)) | |
6 | 5 | ssriv 3921 | . . . 4 ⊢ Q ⊆ (N × N) |
7 | xpss12 5583 | . . . 4 ⊢ ((Q ⊆ (N × N) ∧ Q ⊆ (N × N)) → (Q × Q) ⊆ ((N × N) × (N × N))) | |
8 | 6, 6, 7 | mp2an 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) | |
10 | 4, 8, 9 | mp2an 692 | . 2 ⊢ (([Q] ∘ +pQ ) ↾ (Q × Q)):(Q × Q)⟶Q |
11 | df-plq 10555 | . . 3 ⊢ +Q = (([Q] ∘ +pQ ) ↾ (Q × Q)) | |
12 | 11 | feq1i 6557 | . 2 ⊢ ( +Q :(Q × Q)⟶Q ↔ (([Q] ∘ +pQ ) ↾ (Q × Q)):(Q × Q)⟶Q) |
13 | 10, 12 | mpbir 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 |