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  5479  foeq2  5480  foeq3  5481  nffo  5482  fof  5483  forn  5486  dffo2  5487  dffn4  5489  fores  5493  dff1o2  5512  dff1o3  5513  foimacnv  5525  foun  5526  fconstfvm  5783  dff1o6  5826  fo1st  6224  fo2nd  6225  tposfo2  6334  ctssdc  7188  exmidfodomrlemim  7280  reeff1o  15093