Definition df-fo 5330

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 5322	. 2 wff F : A -onto-> B
5	3, 1	wfn 5319	. . 3 wff F Fn A
6	3	crn 4724	. . . 4 class ran F
7	6, 2	wceq 1395	. . 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  5552  foeq2  5553  foeq3  5554  nffo  5555  fof  5556  forn  5559  dffo2  5560  dffn4  5562  fores  5566  dff1o2  5585  dff1o3  5586  foimacnv  5598  foun  5599  fconstfvm  5867  dff1o6  5912  fo1st  6315  fo2nd  6316  tposfo2  6428  ctssdc  7303  exmidfodomrlemim  7402  reeff1o  15487