![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fores | Structured version Visualization version GIF version |
Description: Restriction of an onto function. (Contributed by NM, 4-Mar-1997.) |
Ref | Expression |
---|---|
fores | ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funres 6598 | . . 3 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴)) | |
2 | 1 | anim1i 613 | . 2 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (Fun (𝐹 ↾ 𝐴) ∧ 𝐴 ⊆ dom 𝐹)) |
3 | df-fn 6554 | . . 3 ⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ (Fun (𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴)) | |
4 | df-ima 5693 | . . . . 5 ⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴) | |
5 | 4 | eqcomi 2736 | . . . 4 ⊢ ran (𝐹 ↾ 𝐴) = (𝐹 “ 𝐴) |
6 | df-fo 6557 | . . . 4 ⊢ ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ ((𝐹 ↾ 𝐴) Fn 𝐴 ∧ ran (𝐹 ↾ 𝐴) = (𝐹 “ 𝐴))) | |
7 | 5, 6 | mpbiran2 708 | . . 3 ⊢ ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ (𝐹 ↾ 𝐴) Fn 𝐴) |
8 | ssdmres 6020 | . . . 4 ⊢ (𝐴 ⊆ dom 𝐹 ↔ dom (𝐹 ↾ 𝐴) = 𝐴) | |
9 | 8 | anbi2i 621 | . . 3 ⊢ ((Fun (𝐹 ↾ 𝐴) ∧ 𝐴 ⊆ dom 𝐹) ↔ (Fun (𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴)) |
10 | 3, 7, 9 | 3bitr4i 302 | . 2 ⊢ ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ (Fun (𝐹 ↾ 𝐴) ∧ 𝐴 ⊆ dom 𝐹)) |
11 | 2, 10 | sylibr 233 | 1 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ⊆ wss 3947 dom cdm 5680 ran crn 5681 ↾ cres 5682 “ cima 5683 Fun wfun 6545 Fn wfn 6546 –onto→wfo 6549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2698 ax-sep 5301 ax-nul 5308 ax-pr 5431 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5151 df-opab 5213 df-xp 5686 df-rel 5687 df-cnv 5688 df-co 5689 df-dm 5690 df-res 5692 df-ima 5693 df-fun 6553 df-fn 6554 df-fo 6557 |
This theorem is referenced by: fimadmfoALT 6825 resdif 6863 f1oweALT 7980 imafiALT 9375 f1opwfi 9386 fodomfi2 10089 fin1a2lem7 10435 znnen 16194 connima 23347 1stcfb 23367 1stckgenlem 23475 qtoprest 23639 re2ndc 24735 uniiccdif 25525 opnmblALT 25550 mbfimaopnlem 25602 ffsrn 32529 cycpmconjvlem 32880 erdszelem2 34807 ivthALT 35824 poimirlem26 37124 poimirlem27 37125 lmhmfgima 42511 |
Copyright terms: Public domain | W3C validator |