![]() |
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 3998 | . . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵) | |
2 | 1 | anim2i 617 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
3 | df-fo 6499 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
4 | df-f 6497 | . 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 3908 ran crn 5632 Fn wfn 6488 ⟶wf 6489 –onto→wfo 6491 |
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 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3445 df-in 3915 df-ss 3925 df-f 6497 df-fo 6499 |
This theorem is referenced by: fofun 6754 fofn 6755 dffo2 6757 foima 6758 focnvimacdmdm 6765 focofo 6766 resdif 6802 fimacnvinrn 7019 fconst5 7151 cocan2 7234 foeqcnvco 7242 soisoi 7269 ffoss 7870 focdmex 7880 opco1 8047 opco2 8048 tposf2 8173 smoiso2 8307 mapfoss 8748 ssdomg 8898 fopwdom 8982 unfilem2 9213 fodomfib 9228 fofinf1o 9229 brwdomn0 9463 fowdom 9465 wdomtr 9469 wdomima2g 9480 fodomfi2 9954 wdomfil 9955 alephiso 9992 iunfictbso 10008 cofsmo 10163 isf32lem10 10256 fin1a2lem7 10300 fodomb 10420 iunfo 10433 tskuni 10677 gruima 10696 gruen 10706 axpre-sup 11063 wrdsymb 14384 supcvg 15695 ruclem13 16078 imasval 17347 imasle 17359 imasaddfnlem 17364 imasaddflem 17366 imasvscafn 17373 imasvscaf 17375 imasless 17376 homadm 17880 homacd 17881 dmaf 17889 cdaf 17890 setcepi 17928 imasmnd2 18547 sursubmefmnd 18660 imasgrp2 18815 mhmid 18821 mhmmnd 18822 mhmfmhm 18823 ghmgrp 18824 efgred2 19488 ghmfghm 19562 ghmcyg 19626 gsumval3 19637 gsumzoppg 19674 gsum2dlem2 19701 imasring 19992 znunit 20917 znrrg 20919 cygznlem2a 20921 cygznlem3 20923 cncmp 22689 cnconn 22719 1stcfb 22742 dfac14 22915 qtopval2 22993 qtopuni 22999 qtopid 23002 qtopcld 23010 qtopcn 23011 qtopeu 23013 qtophmeo 23114 elfm3 23247 ovoliunnul 24817 uniiccdif 24888 dchrzrhcl 26539 lgsdchrval 26648 rpvmasumlem 26781 dchrmusum2 26788 dchrvmasumlem3 26793 dchrisum0ff 26801 dchrisum0flblem1 26802 rpvmasum2 26806 dchrisum0re 26807 dchrisum0lem2a 26811 nodense 26986 bdaydm 27060 bdayelon 27062 grpocl 29287 grporndm 29297 vafval 29390 smfval 29392 nvgf 29405 vsfval 29420 hhssabloilem 30048 pjhf 30495 elunop 30659 unopf1o 30703 cnvunop 30705 pjinvari 30978 foresf1o 31276 rabfodom 31277 iunrdx 31327 xppreima 31407 gsumpart 31739 qtophaus 32245 sigapildsys 32589 carsgclctunlem3 32748 mtyf 33974 poimirlem26 36036 poimirlem27 36037 volsupnfl 36055 cocanfo 36109 exidreslem 36268 rngosn3 36315 rngodm1dm2 36323 founiiun 43295 founiiun0 43308 issalnnd 44481 sge0fodjrnlem 44552 ismeannd 44603 caragenunicl 44660 fcores 45196 fcoresf1lem 45197 fcoresf1 45198 fcoresfo 45200 fargshiftfo 45529 |
Copyright terms: Public domain | W3C validator |