Definition df-fo 5265

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	⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

Detailed syntax breakdown of Definition df-fo

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wfo 5257	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5254	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4665	. . . 4 class ran 𝐹
7	6, 2	wceq 1364	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 104	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 105	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  5477  foeq2  5478  foeq3  5479  nffo  5480  fof  5481  forn  5484  dffo2  5485  dffn4  5487  fores  5491  dff1o2  5510  dff1o3  5511  foimacnv  5523  foun  5524  fconstfvm  5781  dff1o6  5824  fo1st  6216  fo2nd  6217  tposfo2  6326  ctssdc  7180  exmidfodomrlemim  7270  reeff1o  15019