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 4021 | . . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵) | |
2 | 1 | anim2i 618 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
3 | df-fo 6354 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
4 | df-f 6352 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
5 | 2, 3, 4 | 3imtr4i 294 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1531 ⊆ wss 3934 ran crn 5549 Fn wfn 6343 ⟶wf 6344 –onto→wfo 6346 |
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 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-in 3941 df-ss 3950 df-f 6352 df-fo 6354 |
This theorem is referenced by: fofun 6584 fofn 6585 dffo2 6587 foima 6588 resdif 6628 fimacnvinrn 6833 fconst5 6961 cocan2 7040 foeqcnvco 7048 soisoi 7073 ffoss 7639 fornex 7649 algrflem 7811 tposf2 7908 smoiso2 7998 ssdomg 8547 fopwdom 8617 unfilem2 8775 fodomfib 8790 fofinf1o 8791 brwdomn0 9025 fowdom 9027 wdomtr 9031 wdomima2g 9042 fodomfi2 9478 wdomfil 9479 alephiso 9516 iunfictbso 9532 cofsmo 9683 isf32lem10 9776 fin1a2lem7 9820 fodomb 9940 iunfo 9953 tskuni 10197 gruima 10216 gruen 10226 axpre-sup 10583 focdmex 13703 wrdsymb 13885 supcvg 15203 ruclem13 15587 imasval 16776 imasle 16788 imasaddfnlem 16793 imasaddflem 16795 imasvscafn 16802 imasvscaf 16804 imasless 16805 homadm 17292 homacd 17293 dmaf 17301 cdaf 17302 setcepi 17340 imasmnd2 17940 sursubmefmnd 18053 imasgrp2 18206 mhmid 18212 mhmmnd 18213 mhmfmhm 18214 ghmgrp 18215 efgred2 18871 ghmfghm 18943 ghmcyg 19008 gsumval3 19019 gsumzoppg 19056 gsum2dlem2 19083 imasring 19361 znunit 20702 znrrg 20704 cygznlem2a 20706 cygznlem3 20708 cncmp 21992 cnconn 22022 1stcfb 22045 dfac14 22218 qtopval2 22296 qtopuni 22302 qtopid 22305 qtopcld 22313 qtopcn 22314 qtopeu 22316 qtophmeo 22417 elfm3 22550 ovoliunnul 24100 uniiccdif 24171 dchrzrhcl 25813 lgsdchrval 25922 rpvmasumlem 26055 dchrmusum2 26062 dchrvmasumlem3 26067 dchrisum0ff 26075 dchrisum0flblem1 26076 rpvmasum2 26080 dchrisum0re 26081 dchrisum0lem2a 26085 grpocl 28269 grporndm 28279 vafval 28372 smfval 28374 nvgf 28387 vsfval 28402 hhssabloilem 29030 pjhf 29477 elunop 29641 unopf1o 29685 cnvunop 29687 pjinvari 29960 foresf1o 30257 rabfodom 30258 iunrdx 30307 xppreima 30386 qtophaus 31093 sigapildsys 31414 carsgclctunlem3 31571 mtyf 32792 nodense 33189 bdaydm 33237 bdayelon 33239 poimirlem26 34910 poimirlem27 34911 volsupnfl 34929 cocanfo 34985 exidreslem 35147 rngosn3 35194 rngodm1dm2 35202 founiiun 41425 founiiun0 41441 issalnnd 42619 sge0fodjrnlem 42689 ismeannd 42740 caragenunicl 42797 fargshiftfo 43593 |
Copyright terms: Public domain | W3C validator |