![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fofn | Structured version Visualization version GIF version |
Description: An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008.) |
Ref | Expression |
---|---|
fofn | ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fof 6805 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | 1 | ffnd 6717 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fn wfn 6537 –onto→wfo 6540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-v 3471 df-in 3951 df-ss 3961 df-f 6546 df-fo 6548 |
This theorem is referenced by: fodmrnu 6813 foun 6851 fo00 6869 foelcdmi 6954 cbvfo 7292 foeqcnvco 7303 canth 7367 br1steqg 8009 br2ndeqg 8010 1stcof 8017 2ndcof 8018 df1st2 8097 df2nd2 8098 1stconst 8099 2ndconst 8100 fsplit 8116 smoiso2 8383 fodomfi 9341 brwdom2 9588 fodomfi2 10075 fpwwe 10661 imasaddfnlem 17501 imasvscafn 17510 imasleval 17514 dmaf 18029 cdaf 18030 imasmnd2 18722 imasgrp2 19002 efgrelexlemb 19696 efgredeu 19698 imasrng 20108 imasring 20255 znf1o 21472 zzngim 21473 indlcim 21761 1stcfb 23336 upxp 23514 uptx 23516 cnmpt1st 23559 cnmpt2nd 23560 qtoptopon 23595 qtopcld 23604 qtopeu 23607 qtoprest 23608 imastopn 23611 qtophmeo 23708 elfm3 23841 uniiccdif 25494 dirith 27449 nosupno 27623 nosupbday 27625 noinfno 27638 noinfbday 27640 noetasuplem4 27656 noetainflem4 27660 bdayfn 27693 grporn 30318 0vfval 30403 foresf1o 32286 2ndimaxp 32416 2ndresdju 32418 xppreima2 32420 1stpreimas 32469 1stpreima 32470 2ndpreima 32471 fsuppcurry1 32491 fsuppcurry2 32492 ffsrn 32495 gsummpt2d 32741 qusker 33001 imaslmod 33005 qtopt1 33372 qtophaus 33373 circcn 33375 cnre2csqima 33448 sigapildsys 33717 carsgclctunlem3 33876 fnbigcup 35433 filnetlem4 35801 ovoliunnfl 37070 voliunnfl 37072 volsupnfl 37073 ssnnf1octb 44490 nnfoctbdj 45767 fcoreslem4 46371 fcoresf1 46374 fargshiftfo 46705 |
Copyright terms: Public domain | W3C validator |