Definition df-fo 5194

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 5186	. 2 wff F : A -onto-> B
5	3, 1	wfn 5183	. . 3 wff F Fn A
6	3	crn 4605	. . . 4 class ran F
7	6, 2	wceq 1343	. . 3 wff ran F = B
8	5, 7	wa 103	. 2 wff ( F Fn A /\ ran F = B )
9	4, 8	wb 104	1 wff ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )

This definition is referenced by:  foeq1  5406  foeq2  5407  foeq3  5408  nffo  5409  fof  5410  forn  5413  dffo2  5414  dffn4  5416  fores  5419  dff1o2  5437  dff1o3  5438  foimacnv  5450  foun  5451  fconstfvm  5703  dff1o6  5744  fo1st  6125  fo2nd  6126  tposfo2  6235  ctssdc  7078  exmidfodomrlemim  7157  reeff1o  13334