Definition df-fo 5323

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 5315	. 2 wff F : A -onto-> B
5	3, 1	wfn 5312	. . 3 wff F Fn A
6	3	crn 4719	. . . 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  5543  foeq2  5544  foeq3  5545  nffo  5546  fof  5547  forn  5550  dffo2  5551  dffn4  5553  fores  5557  dff1o2  5576  dff1o3  5577  foimacnv  5589  foun  5590  fconstfvm  5856  dff1o6  5899  fo1st  6301  fo2nd  6302  tposfo2  6411  ctssdc  7276  exmidfodomrlemim  7375  reeff1o  15441