![]() |
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 4005 | . . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵) | |
2 | 1 | anim2i 617 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
3 | df-fo 6507 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
4 | df-f 6505 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
5 | 2, 3, 4 | 3imtr4i 291 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ⊆ wss 3913 ran crn 5639 Fn wfn 6496 ⟶wf 6497 –onto→wfo 6499 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3448 df-in 3920 df-ss 3930 df-f 6505 df-fo 6507 |
This theorem is referenced by: fofun 6762 fofn 6763 dffo2 6765 foima 6766 focnvimacdmdm 6773 focofo 6774 resdif 6810 fimacnvinrn 7027 fconst5 7160 cocan2 7243 foeqcnvco 7251 soisoi 7278 ffoss 7883 focdmex 7893 opco1 8060 opco2 8061 tposf2 8186 smoiso2 8320 mapfoss 8797 ssdomg 8947 fopwdom 9031 unfilem2 9262 fodomfib 9277 fofinf1o 9278 brwdomn0 9514 fowdom 9516 wdomtr 9520 wdomima2g 9531 fodomfi2 10005 wdomfil 10006 alephiso 10043 iunfictbso 10059 cofsmo 10214 isf32lem10 10307 fin1a2lem7 10351 fodomb 10471 iunfo 10484 tskuni 10728 gruima 10747 gruen 10757 axpre-sup 11114 wrdsymb 14442 supcvg 15752 ruclem13 16135 imasval 17407 imasle 17419 imasaddfnlem 17424 imasaddflem 17426 imasvscafn 17433 imasvscaf 17435 imasless 17436 homadm 17940 homacd 17941 dmaf 17949 cdaf 17950 setcepi 17988 imasmnd2 18607 sursubmefmnd 18720 imasgrp2 18876 mhmid 18882 mhmmnd 18883 mhmfmhm 18884 ghmgrp 18885 efgred2 19549 ghmfghm 19623 ghmcyg 19687 gsumval3 19698 gsumzoppg 19735 gsum2dlem2 19762 imasring 20059 znunit 21007 znrrg 21009 cygznlem2a 21011 cygznlem3 21013 cncmp 22780 cnconn 22810 1stcfb 22833 dfac14 23006 qtopval2 23084 qtopuni 23090 qtopid 23093 qtopcld 23101 qtopcn 23102 qtopeu 23104 qtophmeo 23205 elfm3 23338 ovoliunnul 24908 uniiccdif 24979 dchrzrhcl 26630 lgsdchrval 26739 rpvmasumlem 26872 dchrmusum2 26879 dchrvmasumlem3 26884 dchrisum0ff 26892 dchrisum0flblem1 26893 rpvmasum2 26897 dchrisum0re 26898 dchrisum0lem2a 26902 nodense 27077 bdaydm 27157 bdayelon 27159 grpocl 29505 grporndm 29515 vafval 29608 smfval 29610 nvgf 29623 vsfval 29638 hhssabloilem 30266 pjhf 30713 elunop 30877 unopf1o 30921 cnvunop 30923 pjinvari 31196 foresf1o 31495 rabfodom 31496 iunrdx 31549 xppreima 31629 gsumpart 31967 qtophaus 32506 sigapildsys 32850 carsgclctunlem3 33009 mtyf 34233 poimirlem26 36177 poimirlem27 36178 volsupnfl 36196 cocanfo 36250 exidreslem 36409 rngosn3 36456 rngodm1dm2 36464 founiiun 43518 founiiun0 43531 issalnnd 44706 sge0fodjrnlem 44777 ismeannd 44828 caragenunicl 44885 fcores 45421 fcoresf1lem 45422 fcoresf1 45423 fcoresfo 45425 fargshiftfo 45754 |
Copyright terms: Public domain | W3C validator |