Definition df-fo 4794

Description: Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). For alternate definitions, see dffo2 5274, dffo3 5423, dffo4 5424, and dffo5 5425. (Contributed by SF, 5-Jan-2015.)

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 4780	. 2 wff F:A-onto->B
5	3, 1	wfn 4777	. . 3 wff F Fn A
6	3	crn 4774	. . . 4 class ran F
7	6, 2	wceq 1642	. . 3 wff ran F = B
8	5, 7	wa 358	. 2 wff (F Fn A /\ ran F = B)
9	4, 8	wb 176	1 wff (F:A-onto->B <-> (F Fn A /\ ran F = B))

This definition is referenced by:  foeq1  5266  foeq2  5267  foeq3  5268  nffo  5269  fof  5270  forn  5273  dffo2  5274  dffn4  5276  fores  5279  dff1o2  5292  dff1o3  5293  foimacnv  5304  f1o0  5320  fconst5  5456  fconstfv  5457  dff1o6  5476  1stfo  5506  2ndfo  5507