Definition df-fo 3202

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 3186	. 2 wff F:A-onto->B
5	3, 1	wfn 3183	. . 3 wff F Fn A
6	3	crn 3177	. . . 4 class ran F
7	6, 2	wceq 958	. . 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 3674  foeq2 3675  foeq3 3676  hbfo 3677  fof 3678  forn 3680  dffo2 3681  fnforn 3683  fores 3687  f1o2 3699  f1o3 3700  f1o5 3703  f1oi 3723  fconst5 3854  fconstfv 3855  f1ofv 3883  f1oweALT 3912  fo1st 4097  fo2nd 4098  fodomr 4489  unfilem2 4561  brdom3 4811  brdom5 4812  brdom4 4813  alephiso 4903  reeff1o 7426  qnnen 7504  ghgrpilem1 8129  ghgrpilem2 8130  ghgrpilem3 8131  ghgrpilem4 8132  pjfo 9643  ghomfo 10386  trnij 10608

Copyright terms: Public domain