Definition df-fo 4145

Description: Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). For alternate definitions, see dffo2 4709, dffo3 4882, dffo4 4883, and dffo5 4884.

Assertion

Ref	Expression
df-fo	|- (F:A-onto->B <-> (F Fn A /\ ran F = B))

Detailed syntax breakdown of Definition df-fo

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	wfo 4129	. 2 wff F:A-onto->B
5	3, 1	wfn 4126	. . 3 wff F Fn A
6	3	crn 4120	. . . 4 class ran F
7	6, 2	wceq 1586	. . 3 wff ran F = B
8	5, 7	wa 337	. 2 wff (F Fn A /\ ran F = B)
9	4, 8	wb 219	1 wff (F:A-onto->B <-> (F Fn A /\ ran F = B))

This definition is referenced by:  foeq1 4701  foeq2 4702  foeq3 4703  hbfo 4704  fof 4705  forn 4708  dffo2 4709  dffn4 4711  fores 4715  dff1o2 4727  dff1o3 4728  foimacnv 4740  fconst5 4916  fconstfv 4917  dff1o6 4948  f1oweALT 4980  fo1st 5138  fo2nd 5139  fodomr 5716  unfilem2 5861  alephiso 6221  brdom3 6377  brdom5 6378  brdom4 6379  reeff1o 9089  qnnen 9171  qnnenOLD 9172  ghgrpilem1 10310  ghgrpilem2 10311  ghgrpilem3 10312  ghgrpilem4 10313  gafo 10320  minvec34 10768  pjfoi 12115  ghomfo 14371  axbday 14681  fobigcup 14761  dff1o6f 15128  trnij 15807  fictb 16195  hartoglem 16207  hscptsscld 16258

Copyright terms: Public domain