Definition df-fo 5339

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 5331	. 2 wff F : A -onto-> B
5	3, 1	wfn 5328	. . 3 wff F Fn A
6	3	crn 4732	. . . 4 class ran F
7	6, 2	wceq 1398	. . 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  5564  foeq2  5565  foeq3  5566  nffo  5567  fof  5568  forn  5571  dffo2  5572  dffn4  5574  fores  5578  dff1o2  5597  dff1o3  5598  foimacnv  5610  foun  5611  fconstfvm  5880  dff1o6  5927  fo1st  6329  fo2nd  6330  tposfo2  6476  ctssdc  7372  exmidfodomrlemim  7472  reeff1o  15584