Definition df-fo 5224

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 5216	. 2 wff F : A -onto-> B
5	3, 1	wfn 5213	. . 3 wff F Fn A
6	3	crn 4629	. . . 4 class ran F
7	6, 2	wceq 1353	. . 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  5436  foeq2  5437  foeq3  5438  nffo  5439  fof  5440  forn  5443  dffo2  5444  dffn4  5446  fores  5449  dff1o2  5468  dff1o3  5469  foimacnv  5481  foun  5482  fconstfvm  5736  dff1o6  5779  fo1st  6160  fo2nd  6161  tposfo2  6270  ctssdc  7114  exmidfodomrlemim  7202  reeff1o  14233