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 6382 | . . 3 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴)) | |
2 | 1 | anim1i 618 | . 2 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (Fun (𝐹 ↾ 𝐴) ∧ 𝐴 ⊆ dom 𝐹)) |
3 | df-fn 6343 | . . 3 ⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ (Fun (𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴)) | |
4 | df-ima 5539 | . . . . 5 ⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴) | |
5 | 4 | eqcomi 2748 | . . . 4 ⊢ ran (𝐹 ↾ 𝐴) = (𝐹 “ 𝐴) |
6 | df-fo 6346 | . . . 4 ⊢ ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ ((𝐹 ↾ 𝐴) Fn 𝐴 ∧ ran (𝐹 ↾ 𝐴) = (𝐹 “ 𝐴))) | |
7 | 5, 6 | mpbiran2 710 | . . 3 ⊢ ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ (𝐹 ↾ 𝐴) Fn 𝐴) |
8 | ssdmres 5849 | . . . 4 ⊢ (𝐴 ⊆ dom 𝐹 ↔ dom (𝐹 ↾ 𝐴) = 𝐴) | |
9 | 8 | anbi2i 626 | . . 3 ⊢ ((Fun (𝐹 ↾ 𝐴) ∧ 𝐴 ⊆ dom 𝐹) ↔ (Fun (𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴)) |
10 | 3, 7, 9 | 3bitr4i 306 | . 2 ⊢ ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ (Fun (𝐹 ↾ 𝐴) ∧ 𝐴 ⊆ dom 𝐹)) |
11 | 2, 10 | sylibr 237 | 1 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1542 ⊆ wss 3844 dom cdm 5526 ran crn 5527 ↾ cres 5528 “ cima 5529 Fun wfun 6334 Fn wfn 6335 –onto→wfo 6338 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 ax-sep 5168 ax-nul 5175 ax-pr 5297 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-ral 3059 df-rex 3060 df-v 3401 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-nul 4213 df-if 4416 df-sn 4518 df-pr 4520 df-op 4524 df-br 5032 df-opab 5094 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-res 5538 df-ima 5539 df-fun 6342 df-fn 6343 df-fo 6346 |
This theorem is referenced by: fimadmfoALT 6604 resdif 6641 f1oweALT 7701 imafiOLD 8893 f1opwfi 8904 fodomfi2 9563 fin1a2lem7 9909 znnen 15660 connima 22179 1stcfb 22199 1stckgenlem 22307 qtoprest 22471 re2ndc 23556 uniiccdif 24333 opnmblALT 24358 mbfimaopnlem 24410 ffsrn 30642 cycpmconjvlem 30988 erdszelem2 32728 ivthALT 34170 poimirlem26 35449 poimirlem27 35450 lmhmfgima 40504 |
Copyright terms: Public domain | W3C validator |