Theorem fof 3672

Description: An onto mapping is a mapping.

Assertion

Ref	Expression
fof	|- (F:A-onto->B -> F:A-->B)

Proof of Theorem fof

Step	Hyp	Ref	Expression
1		eqimss 2109	. . 3 |- (ran F = B -> ran F (_ B)
2	1	anim2i 335	. 2 |- ((F Fn A /\ ran F = B) -> (F Fn A /\ ran F (_ B))
3		df-fo 3196	. 2 |- (F:A-onto->B <-> (F Fn A /\ ran F = B))
4		df-f 3194	. 2 |- (F:A-->B <-> (F Fn A /\ ran F (_ B))
5	2, 3, 4	3imtr4 219	1 |- (F:A-onto->B -> F:A-->B)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 956   (_ wss 2047  ran crn 3171   Fn wfn 3177  -->wf 3178  -onto->wfo 3180

This theorem is referenced by:  fofun 3673  dffo2 3675  foima 3676  fornex 3679  fodmrnu 3680  ffoss 3711  fo00 3715  fconst5 3848  fconstfv 3849  cbvfo 3885  canth 3907  2ndconst 4097  1stcof 4101  df1st2 4126  df2nd2 4127  mapsn 4345  ssdomg 4408  unfilem2 4549  fiint 4559  fiintOLD 4560  fodomfiOLD 4566  fodomfibOLD 4567  fodom 4798  fodomb 4800  alephiso 4892  ruclem39 7548  infmap2lem2 7580  grpcl 8044  grprndm 8054  grprn 8056  resgrprn 8095  subgres 8117  issubgi 8122  vcoprnelem 8197  vafval 8222  smfval 8224  0vfval 8225  nvgf 8237  vsfval 8254  pjft 9653  elunopt 9799  unopf1ot 9840  cnvunopt 9842  pjinvar 10119  ghomfo 10391  ghomcl 10392  ghomgsg 10395  ghomf1olem 10396  cayleylem3 10411  domval 10655  codval 10656  idval 10657  cmpval 10658

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053  df-f 3194  df-fo 3196

Copyright terms: Public domain