Definition df-fo 3196

Description: Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow).

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 3180	. 2 wff F:A-onto->B
5	3, 1	wfn 3177	. . 3 wff F Fn A
6	3	crn 3171	. . . 4 class ran F
7	6, 2	wceq 956	. . 3 wff ran F = B
8	5, 7	wa 223	. 2 wff (F Fn A /\ ran F = B)
9	4, 8	wb 146	1 wff (F:A-onto->B <-> (F Fn A /\ ran F = B))

This definition is referenced by:  foeq1 3668  foeq2 3669  foeq3 3670  hbfo 3671  fof 3672  forn 3674  dffo2 3675  fnforn 3677  fores 3681  f1o2 3693  f1o3 3694  f1o5 3697  f1oi 3717  fconst5 3848  fconstfv 3849  f1ofv 3877  f1oweALT 3906  fo1st 4091  fo2nd 4092  fodomr 4483  unfilem2 4549  brdom3 4801  brdom5 4802  brdom4 4803  alephiso 4892  reeff1o 7426  qnnen 7503  ghgrpilem1 8133  ghgrpilem2 8134  ghgrpilem3 8135  ghgrpilem4 8136  pjfo 9648  ghomfo 10391  trnij 10637

Copyright terms: Public domain