Definition df-fo 3277

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 3783, dffo3 3933, dffo4 3934, and dffo5 3935.

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 3261	. 2 wff F:A-onto->B
5	3, 1	wfn 3258	. . 3 wff F Fn A
6	3	crn 3252	. . . 4 class ran F
7	6, 2	wceq 992	. . 3 wff ran F = B
8	5, 7	wa 221	. 2 wff (F Fn A /\ ran F = B)
9	4, 8	wb 144	1 wff (F:A-onto->B <-> (F Fn A /\ ran F = B))

This definition is referenced by:  foeq1 3775  foeq2 3776  foeq3 3777  hbfo 3778  fof 3779  forn 3782  dffo2 3783  dffn4 3785  fores 3789  dff1o2 3801  dff1o3 3802  dff1o5 3805  foimacnv 3814  f1oi 3828  fconst5 3962  fconstfv 3963  dff1o6 3991  f1oweALT 4020  fo1st 4152  fo2nd 4153  fodomr 4628  unfilem2 4695  brdom3 4947  brdom5 4948  brdom4 4949  alephiso 5042  reeff1o 7634  qnnen 7715  ghgrpilem1 8374  ghgrpilem2 8375  ghgrpilem3 8376  ghgrpilem4 8377  pjfoi 9926  ghomfo 10676  trnij 11160  fictb 11423  hartoglem 11435  hscptsscld 11491  gafo 11773

Copyright terms: Public domain