Definition df-fo 5296

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 5288	. 2 wff F : A -onto-> B
5	3, 1	wfn 5285	. . 3 wff F Fn A
6	3	crn 4694	. . . 4 class ran F
7	6, 2	wceq 1373	. . 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  5516  foeq2  5517  foeq3  5518  nffo  5519  fof  5520  forn  5523  dffo2  5524  dffn4  5526  fores  5530  dff1o2  5549  dff1o3  5550  foimacnv  5562  foun  5563  fconstfvm  5825  dff1o6  5868  fo1st  6266  fo2nd  6267  tposfo2  6376  ctssdc  7241  exmidfodomrlemim  7340  reeff1o  15360