Definition df-fo 5234

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 5226	. 2 wff F : A -onto-> B
5	3, 1	wfn 5223	. . 3 wff F Fn A
6	3	crn 4639	. . . 4 class ran F
7	6, 2	wceq 1363	. . 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  5446  foeq2  5447  foeq3  5448  nffo  5449  fof  5450  forn  5453  dffo2  5454  dffn4  5456  fores  5459  dff1o2  5478  dff1o3  5479  foimacnv  5491  foun  5492  fconstfvm  5747  dff1o6  5790  fo1st  6171  fo2nd  6172  tposfo2  6281  ctssdc  7125  exmidfodomrlemim  7213  reeff1o  14465