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 10714 | . . . 4 ⊢ [Q]:(N × N)⟶Q | |
2 | addpqf 10728 | . . . 4 ⊢ +pQ :((N × N) × (N × N))⟶(N × N) | |
3 | fco 6642 | . . . 4 ⊢ (([Q]:(N × N)⟶Q ∧ +pQ :((N × N) × (N × N))⟶(N × N)) → ([Q] ∘ +pQ ):((N × N) × (N × N))⟶Q) | |
4 | 1, 2, 3 | mp2an 688 | . . 3 ⊢ ([Q] ∘ +pQ ):((N × N) × (N × N))⟶Q |
5 | elpqn 10709 | . . . . 5 ⊢ (𝑥 ∈ Q → 𝑥 ∈ (N × N)) | |
6 | 5 | ssriv 3927 | . . . 4 ⊢ Q ⊆ (N × N) |
7 | xpss12 5606 | . . . 4 ⊢ ((Q ⊆ (N × N) ∧ Q ⊆ (N × N)) → (Q × Q) ⊆ ((N × N) × (N × N))) | |
8 | 6, 6, 7 | mp2an 688 | . . 3 ⊢ (Q × Q) ⊆ ((N × N) × (N × N)) |
9 | fssres 6658 | . . 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 688 | . 2 ⊢ (([Q] ∘ +pQ ) ↾ (Q × Q)):(Q × Q)⟶Q |
11 | df-plq 10698 | . . 3 ⊢ +Q = (([Q] ∘ +pQ ) ↾ (Q × Q)) | |
12 | 11 | feq1i 6609 | . 2 ⊢ ( +Q :(Q × Q)⟶Q ↔ (([Q] ∘ +pQ ) ↾ (Q × Q)):(Q × Q)⟶Q) |
13 | 10, 12 | mpbir 230 | 1 ⊢ +Q :(Q × Q)⟶Q |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3889 × cxp 5589 ↾ cres 5593 ∘ ccom 5595 ⟶wf 6443 Ncnpi 10628 +pQ cplpq 10632 Qcnq 10636 [Q]cerq 10638 +Q cplq 10639 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-10 2132 ax-11 2149 ax-12 2166 ax-ext 2704 ax-sep 5226 ax-nul 5233 ax-pr 5355 ax-un 7608 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2063 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2884 df-ne 2939 df-ral 3060 df-rex 3069 df-rmo 3222 df-reu 3223 df-rab 3224 df-v 3436 df-sbc 3719 df-csb 3835 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3908 df-nul 4260 df-if 4463 df-pw 4538 df-sn 4565 df-pr 4567 df-op 4571 df-uni 4842 df-iun 4929 df-br 5078 df-opab 5140 df-mpt 5161 df-tr 5195 df-id 5491 df-eprel 5497 df-po 5505 df-so 5506 df-fr 5546 df-we 5548 df-xp 5597 df-rel 5598 df-cnv 5599 df-co 5600 df-dm 5601 df-rn 5602 df-res 5603 df-ima 5604 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6399 df-fun 6449 df-fn 6450 df-f 6451 df-f1 6452 df-fo 6453 df-f1o 6454 df-fv 6455 df-ov 7298 df-oprab 7299 df-mpo 7300 df-om 7733 df-1st 7851 df-2nd 7852 df-frecs 8117 df-wrecs 8148 df-recs 8222 df-rdg 8261 df-1o 8317 df-oadd 8321 df-omul 8322 df-er 8518 df-ni 10656 df-pli 10657 df-mi 10658 df-lti 10659 df-plpq 10692 df-enq 10695 df-nq 10696 df-erq 10697 df-plq 10698 df-1nq 10700 |
This theorem is referenced by: addcomnq 10735 adderpq 10740 addassnq 10742 distrnq 10745 ltanq 10755 ltexnq 10759 nsmallnq 10761 ltbtwnnq 10762 prlem934 10817 ltaddpr 10818 ltexprlem2 10821 ltexprlem3 10822 ltexprlem4 10823 ltexprlem6 10825 ltexprlem7 10826 prlem936 10831 |
Copyright terms: Public domain | W3C validator |