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 3620 | . . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵) | |
2 | 1 | anim2i 591 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
3 | df-fo 5810 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
4 | df-f 5808 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
5 | 2, 3, 4 | 3imtr4i 280 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ⊆ wss 3540 ran crn 5039 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: fofun 6029 fofn 6030 dffo2 6032 foima 6033 resdif 6070 fimacnvinrn 6256 fconst5 6376 cocan2 6447 foeqcnvco 6455 soisoi 6478 ffoss 7020 fornex 7028 algrflem 7173 tposf2 7263 smoiso2 7353 mapsn 7785 ssdomg 7887 fopwdom 7953 unfilem2 8110 fodomfib 8125 fofinf1o 8126 brwdomn0 8357 fowdom 8359 wdomtr 8363 wdomima2g 8374 fodomfi2 8766 wdomfil 8767 alephiso 8804 iunfictbso 8820 cofsmo 8974 isf32lem10 9067 fin1a2lem7 9111 fodomb 9229 iunfo 9240 tskuni 9484 gruima 9503 gruen 9513 axpre-sup 9869 focdmex 13001 supcvg 14427 ruclem13 14810 imasval 15994 imasle 16006 imasaddfnlem 16011 imasaddflem 16013 imasvscafn 16020 imasvscaf 16022 imasless 16023 homadm 16513 homacd 16514 dmaf 16522 cdaf 16523 setcepi 16561 imasmnd2 17150 imasgrp2 17353 mhmid 17359 mhmmnd 17360 mhmfmhm 17361 ghmgrp 17362 efgred2 17989 ghmfghm 18059 ghmcyg 18120 gsumval3 18131 gsumzoppg 18167 gsum2dlem2 18193 imasring 18442 znunit 19731 znrrg 19733 cygznlem2a 19735 cygznlem3 19737 cncmp 21005 cnconn 21035 1stcfb 21058 dfac14 21231 qtopval2 21309 qtopuni 21315 qtopid 21318 qtopcld 21326 qtopcn 21327 qtopeu 21329 qtophmeo 21430 elfm3 21564 ovoliunnul 23082 uniiccdif 23152 dchrzrhcl 24770 lgsdchrval 24879 rpvmasumlem 24976 dchrmusum2 24983 dchrvmasumlem3 24988 dchrisum0ff 24996 dchrisum0flblem1 24997 rpvmasum2 25001 dchrisum0re 25002 dchrisum0lem2a 25006 fargshiftfo 26166 grpocl 26738 grporndm 26748 vafval 26842 smfval 26844 nvgf 26857 vsfval 26872 hhssabloilem 27502 pjhf 27951 elunop 28115 unopf1o 28159 cnvunop 28161 pjinvari 28434 foresf1o 28727 rabfodom 28728 iunrdx 28764 xppreima 28829 qtophaus 29231 sigapildsys 29552 carsgclctunlem3 29709 mtyf 30703 bdaydm 31077 poimirlem26 32605 poimirlem27 32606 volsupnfl 32624 cocanfo 32682 exidreslem 32846 rngosn3 32893 rngodm1dm2 32901 founiiun 38355 founiiun0 38372 mapsnd 38383 issalnnd 39239 sge0fodjrnlem 39309 ismeannd 39360 caragenunicl 39414 |
Copyright terms: Public domain | W3C validator |