| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fof | Structured version Visualization version GIF version | ||
| Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.) |
| Ref | Expression |
|---|---|
| fof | ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqimss 4042 | . . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵) | |
| 2 | 1 | anim2i 617 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
| 3 | df-fo 6567 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
| 4 | df-f 6565 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
| 5 | 2, 3, 4 | 3imtr4i 292 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ⊆ wss 3951 ran crn 5686 Fn wfn 6556 ⟶wf 6557 –onto→wfo 6559 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ss 3968 df-f 6565 df-fo 6567 |
| This theorem is referenced by: fofun 6821 fofn 6822 dffo2 6824 foima 6825 focnvimacdmdm 6832 focofo 6833 resdif 6869 fimacnvinrn 7091 fompt 7138 fconst5 7226 cocan2 7312 foeqcnvco 7320 soisoi 7348 ffoss 7970 focdmex 7980 opco1 8148 opco2 8149 tposf2 8275 smoiso2 8409 mapfoss 8892 ssdomg 9040 fopwdom 9120 unfilem2 9344 fodomfib 9369 fodomfibOLD 9371 fofinf1o 9372 brwdomn0 9609 fowdom 9611 wdomtr 9615 wdomima2g 9626 fodomfi2 10100 wdomfil 10101 alephiso 10138 iunfictbso 10154 cofsmo 10309 isf32lem10 10402 fin1a2lem7 10446 fodomb 10566 iunfo 10579 tskuni 10823 gruima 10842 gruen 10852 axpre-sup 11209 wrdsymb 14580 supcvg 15892 ruclem13 16278 imasval 17556 imasle 17568 imasaddfnlem 17573 imasaddflem 17575 imasvscafn 17582 imasvscaf 17584 imasless 17585 homadm 18085 homacd 18086 dmaf 18094 cdaf 18095 setcepi 18133 imasmnd2 18787 sursubmefmnd 18909 imasgrp2 19073 mhmid 19081 mhmmnd 19082 mhmfmhm 19083 ghmgrp 19084 efgred2 19771 ghmfghm 19848 ghmcyg 19914 gsumval3 19925 gsumzoppg 19962 gsum2dlem2 19989 imasring 20327 znunit 21582 znrrg 21584 cygznlem2a 21586 cygznlem3 21588 cncmp 23400 cnconn 23430 1stcfb 23453 dfac14 23626 qtopval2 23704 qtopuni 23710 qtopid 23713 qtopcld 23721 qtopcn 23722 qtopeu 23724 qtophmeo 23825 elfm3 23958 ovoliunnul 25542 uniiccdif 25613 dchrzrhcl 27289 lgsdchrval 27398 rpvmasumlem 27531 dchrmusum2 27538 dchrvmasumlem3 27543 dchrisum0ff 27551 dchrisum0flblem1 27552 rpvmasum2 27556 dchrisum0re 27557 dchrisum0lem2a 27561 nodense 27737 bdaydm 27819 bdayelon 27821 om2noseqlt 28305 om2noseqlt2 28306 om2noseqf1o 28307 noseqrdgfn 28312 grpocl 30519 grporndm 30529 vafval 30622 smfval 30624 nvgf 30637 vsfval 30652 hhssabloilem 31280 pjhf 31727 elunop 31891 unopf1o 31935 cnvunop 31937 pjinvari 32210 foresf1o 32523 rabfodom 32524 iunrdx 32576 xppreima 32655 gsumpart 33060 imasmhm 33382 imasghm 33383 imasrhm 33384 qtophaus 33835 sigapildsys 34163 carsgclctunlem3 34322 mtyf 35557 poimirlem26 37653 poimirlem27 37654 volsupnfl 37672 cocanfo 37726 exidreslem 37884 rngosn3 37931 rngodm1dm2 37939 founiiun 45184 founiiun0 45195 issalnnd 46360 sge0fodjrnlem 46431 ismeannd 46482 caragenunicl 46539 fcores 47079 fcoresf1lem 47080 fcoresf1 47081 fcoresfo 47083 3f1oss1 47087 fargshiftfo 47429 |
| Copyright terms: Public domain | W3C validator |