Definition df-fo 5276

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 5268	. 2 wff F : A -onto-> B
5	3, 1	wfn 5265	. . 3 wff F Fn A
6	3	crn 4675	. . . 4 class ran F
7	6, 2	wceq 1372	. . 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  5493  foeq2  5494  foeq3  5495  nffo  5496  fof  5497  forn  5500  dffo2  5501  dffn4  5503  fores  5507  dff1o2  5526  dff1o3  5527  foimacnv  5539  foun  5540  fconstfvm  5801  dff1o6  5844  fo1st  6242  fo2nd  6243  tposfo2  6352  ctssdc  7214  exmidfodomrlemim  7308  reeff1o  15216