Theorem fof 6805

Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
fof	⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Proof of Theorem fof

Step	Hyp	Ref	Expression
1		eqimss 4036	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 616	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 6548	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 6546	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 292	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534   ⊆ wss 3945  ran crn 5673   Fn wfn 6537  ⟶wf 6538  –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 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-in 3952  df-ss 3962  df-f 6546  df-fo 6548

This theorem is referenced by:  fofun  6806  fofn  6807  dffo2  6809  foima  6810  focnvimacdmdm  6817  focofo  6818  resdif  6854  fimacnvinrn  7075  fompt  7122  fconst5  7212  cocan2  7295  foeqcnvco  7303  soisoi  7330  ffoss  7943  focdmex  7953  opco1  8122  opco2  8123  tposf2  8249  smoiso2  8383  mapfoss  8864  ssdomg  9014  fopwdom  9098  unfilem2  9329  fodomfib  9344  fofinf1o  9345  brwdomn0  9586  fowdom  9588  wdomtr  9592  wdomima2g  9603  fodomfi2  10077  wdomfil  10078  alephiso  10115  iunfictbso  10131  cofsmo  10286  isf32lem10  10379  fin1a2lem7  10423  fodomb  10543  iunfo  10556  tskuni  10800  gruima  10819  gruen  10829  axpre-sup  11186  wrdsymb  14518  supcvg  15828  ruclem13  16212  imasval  17486  imasle  17498  imasaddfnlem  17503  imasaddflem  17505  imasvscafn  17512  imasvscaf  17514  imasless  17515  homadm  18022  homacd  18023  dmaf  18031  cdaf  18032  setcepi  18070  imasmnd2  18724  sursubmefmnd  18841  imasgrp2  19004  mhmid  19012  mhmmnd  19013  mhmfmhm  19014  ghmgrp  19015  efgred2  19701  ghmfghm  19778  ghmcyg  19844  gsumval3  19855  gsumzoppg  19892  gsum2dlem2  19919  imasring  20259  znunit  21490  znrrg  21492  cygznlem2a  21494  cygznlem3  21496  cncmp  23289  cnconn  23319  1stcfb  23342  dfac14  23515  qtopval2  23593  qtopuni  23599  qtopid  23602  qtopcld  23610  qtopcn  23611  qtopeu  23613  qtophmeo  23714  elfm3  23847  ovoliunnul  25429  uniiccdif  25500  dchrzrhcl  27171  lgsdchrval  27280  rpvmasumlem  27413  dchrmusum2  27420  dchrvmasumlem3  27425  dchrisum0ff  27433  dchrisum0flblem1  27434  rpvmasum2  27438  dchrisum0re  27439  dchrisum0lem2a  27443  nodense  27618  bdaydm  27700  bdayelon  27702  om2noseqlt  28165  om2noseqlt2  28166  om2noseqf1o  28167  noseqrdgfn  28172  grpocl  30303  grporndm  30313  vafval  30406  smfval  30408  nvgf  30421  vsfval  30436  hhssabloilem  31064  pjhf  31511  elunop  31675  unopf1o  31719  cnvunop  31721  pjinvari  31994  foresf1o  32293  rabfodom  32294  iunrdx  32347  xppreima  32425  gsumpart  32763  imasmhm  33060  imasghm  33061  imasrhm  33062  qtophaus  33431  sigapildsys  33775  carsgclctunlem3  33934  mtyf  35156  poimirlem26  37113  poimirlem27  37114  volsupnfl  37132  cocanfo  37186  exidreslem  37344  rngosn3  37391  rngodm1dm2  37399  founiiun  44546  founiiun0  44557  issalnnd  45727  sge0fodjrnlem  45798  ismeannd  45849  caragenunicl  45906  fcores  46443  fcoresf1lem  46444  fcoresf1  46445  fcoresfo  46447  fargshiftfo  46776

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »