Definition df-fo 2436

Description: Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27.

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 2420	. 2 wff F:A–onto→B
5	3, 1	wfn 2417	. . 3 wff F Fn A
6	3	crn 2411	. . . 4 class ran F
7	6, 2	wceq 1091	. . 3 wff ran F = B
8	5, 7	wa 196	. 2 wff (F Fn A ∧ ran F = B)
9	4, 8	wb 127	1 wff (F:A–onto→B ↔ (F Fn A ∧ ran F = B))

This definition is referenced by:  foeq1 2784  foeq2 2785  foeq3 2786  hbfo 2787  fof 2788  forn 2789  fnforn 2791  fores 2794  f1o2 2804  f1o3 2805  f1o5 2808  f1oi 2825  fconstfv 2903  f1oweOLD 2944  fo1st 3094  fo2nd 3095  unfilem2 3439  fodomb 3615  alephiso 3697  qnnen 4931

metamath.org