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 6028 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | ffn 5958 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fn wfn 5799 ⟶wf 5800 –onto→wfo 5802 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-in 3547 df-ss 3554 df-f 5808 df-fo 5810 |
This theorem is referenced by: fodmrnu 6036 foun 6068 fo00 6084 foelrni 6154 cbvfo 6444 foeqcnvco 6455 canth 6508 1stcof 7087 2ndcof 7088 df1st2 7150 df2nd2 7151 1stconst 7152 2ndconst 7153 fsplit 7169 smoiso2 7353 fodomfi 8124 brwdom2 8361 fodomfi2 8766 fpwwe 9347 imasaddfnlem 16011 imasvscafn 16020 imasleval 16024 dmaf 16522 cdaf 16523 imasmnd2 17150 imasgrp2 17353 efgrelexlemb 17986 efgredeu 17988 imasring 18442 znf1o 19719 zzngim 19720 indlcim 19998 1stcfb 21058 upxp 21236 uptx 21238 cnmpt1st 21281 cnmpt2nd 21282 qtoptopon 21317 qtopcld 21326 qtopeu 21329 qtoprest 21330 imastopn 21333 qtophmeo 21430 elfm3 21564 uniiccdif 23152 dirith 25018 fargshiftfo 26166 grporn 26759 0vfval 26845 foresf1o 28727 xppreima2 28830 1stpreimas 28866 1stpreima 28867 2ndpreima 28868 ffsrn 28892 gsummpt2d 29112 qtopt1 29230 qtophaus 29231 circcn 29233 cnre2csqima 29285 sigapildsys 29552 carsgclctunlem3 29709 br1steq 30917 br2ndeq 30918 fnbigcup 31178 filnetlem4 31546 ovoliunnfl 32621 voliunnfl 32623 volsupnfl 32624 ssnnf1octb 38377 nnfoctbdj 39349 |
Copyright terms: Public domain | W3C validator |