Definition df-fo 5087

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 5079	. 2 wff F : A -onto-> B
5	3, 1	wfn 5076	. . 3 wff F Fn A
6	3	crn 4500	. . . 4 class ran F
7	6, 2	wceq 1314	. . 3 wff ran F = B
8	5, 7	wa 103	. 2 wff ( F Fn A /\ ran F = B )
9	4, 8	wb 104	1 wff ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )

This definition is referenced by:  foeq1  5299  foeq2  5300  foeq3  5301  nffo  5302  fof  5303  forn  5306  dffo2  5307  dffn4  5309  fores  5312  dff1o2  5328  dff1o3  5329  foimacnv  5341  foun  5342  fconstfvm  5592  dff1o6  5631  fo1st  6009  fo2nd  6010  tposfo2  6118  ctssdc  6950  exmidfodomrlemim  7005