Definition df-fo 5261

Description: Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). (Contributed by NM, 1-Aug-1994.)

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 5253	. 2 wff F : A -onto-> B
5	3, 1	wfn 5250	. . 3 wff F Fn A
6	3	crn 4661	. . . 4 class ran F
7	6, 2	wceq 1364	. . 3 wff ran F = B
8	5, 7	wa 104	. 2 wff ( F Fn A /\ ran F = B )
9	4, 8	wb 105	1 wff ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )

This definition is referenced by:  foeq1  5473  foeq2  5474  foeq3  5475  nffo  5476  fof  5477  forn  5480  dffo2  5481  dffn4  5483  fores  5487  dff1o2  5506  dff1o3  5507  foimacnv  5519  foun  5520  fconstfvm  5777  dff1o6  5820  fo1st  6212  fo2nd  6213  tposfo2  6322  ctssdc  7174  exmidfodomrlemim  7263  reeff1o  14949