Theorem fof 3663

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 2105	. . 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 3191	. 2 |- (F:A-onto->B <-> (F Fn A /\ ran F = B))
4		df-f 3189	. 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 954   (_ wss 2043  ran crn 3166   Fn wfn 3172  -->wf 3173  -onto->wfo 3175

This theorem is referenced by:  fofun 3664  dffo2 3666  foima 3667  fornex 3670  fodmrnu 3671  ffoss 3702  fo00 3706  fconst5 3839  fconstfv 3840  cbvfo 3876  canth 3898  2ndconst 4087  1stcof 4091  df1st2 4116  df2nd2 4117  mapsn 4335  ssdomg 4395  unfilem2 4531  fiint 4540  fodomfi 4546  fodomfib 4547  fodom 4778  fodomb 4780  alephiso 4872  ruclem39 7499  infmap2lem2 7530  grpcl 7994  grprndm 8004  grprn 8006  resgrprn 8045  resgrprnOLD 8046  subgres 8069  issubgi 8074  vcoprnelem 8149  vafval 8174  smfval 8176  0vfval 8177  nvgf 8189  vsfval 8206  pjft 9593  elunopt 9739  unopf1ot 9779  cnvunopt 9781  pjinvar 10057  ghomfo 10325  ghomcl 10326  ghomgsg 10329  ghomf1olem 10330  cayleylem3 10345  domval 10535  codval 10536  idval 10537  cmpval 10538

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049  df-f 3189  df-fo 3191

Copyright terms: Public domain