Theorem fof 4617

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 2665	. . 3 |- (ran F = B -> ran F C_ B)
2	1	anim2i 362	. 2 |- ((F Fn A /\ ran F = B) -> (F Fn A /\ ran F C_ B))
3		df-fo 4012	. 2 |- (F:A-onto->B <-> (F Fn A /\ ran F = B))
4		df-f 4010	. 2 |- (F:A-->B <-> (F Fn A /\ ran F C_ B))
5	2, 3, 4	3imtr4i 236	1 |- (F:A-onto->B -> F:A-->B)

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298   C_ wss 2593  ran crn 3987   Fn wfn 3993  -->wf 3994  -onto->wfo 3996

This theorem is referenced by:  fofun 4618  fofn 4619  dffo2 4621  foima 4622  fornex 4625  resdif 4659  ffoss 4665  fconst5 4824  fconstfv 4825  cbvfo 4861  canth 5112  mapsn 5404  ssdomg 5467  unfilem2 5642  fiint 5650  fodomfi 5656  fodomfib 5657  hartoglem 5692  fodom 5960  fodomb 5962  alephiso 6040  ruclem39 8817  infmap2lem2 8849  grpcl 9324  grprndm 9334  resgrprn 9403  subgres 9426  issubgi 9431  ssga 9455  vafval 9554  smfval 9556  nvgf 9569  vsfval 9586  tx1cn 10223  tx2cn 10224  elfilmap3 10314  rnplrnml0 10402  on1el3 10412  pjf 11288  elunop 11436  unopf1o 11477  cnvunop 11479  pjinvari 11764  ghomfo 13634  ghomcl 13635  ghomgsg 13636  ghomf1olem 13637  bdaydm 14015  surrc2 14390  injsurinj 14487  dmrngrp 14699  rnplrnml3 14768  extopgrp 14980  domval 15070  codval 15071  idval 15072  cmpval 15073  issubcat 15193  hartoglemOLD 15383  exidreslem 16030

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-in 2603  df-ss 2605  df-f 4010  df-fo 4012

Copyright terms: Public domain