Definition df-fo 5277

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 5269	. 2 wff F : A -onto-> B
5	3, 1	wfn 5266	. . 3 wff F Fn A
6	3	crn 4676	. . . 4 class ran F
7	6, 2	wceq 1373	. . 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  5494  foeq2  5495  foeq3  5496  nffo  5497  fof  5498  forn  5501  dffo2  5502  dffn4  5504  fores  5508  dff1o2  5527  dff1o3  5528  foimacnv  5540  foun  5541  fconstfvm  5802  dff1o6  5845  fo1st  6243  fo2nd  6244  tposfo2  6353  ctssdc  7215  exmidfodomrlemim  7309  reeff1o  15245