Definition df-fo 4793

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 5273, dffo3 5422, dffo4 5423, and dffo5 5424. (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 4779	. 2 wff F:A-onto->B
5	3, 1	wfn 4776	. . 3 wff F Fn A
6	3	crn 4773	. . . 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  5265  foeq2  5266  foeq3  5267  nffo  5268  fof  5269  forn  5272  dffo2  5273  dffn4  5275  fores  5278  dff1o2  5291  dff1o3  5292  foimacnv  5303  f1o0  5319  fconst5  5455  fconstfv  5456  dff1o6  5475  1stfo  5505  2ndfo  5506