Definition df-fo 5324

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 5316	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5313	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4720	. . . 4 class ran 𝐹
7	6, 2	wceq 1395	. . 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  5546  foeq2  5547  foeq3  5548  nffo  5549  fof  5550  forn  5553  dffo2  5554  dffn4  5556  fores  5560  dff1o2  5579  dff1o3  5580  foimacnv  5592  foun  5593  fconstfvm  5861  dff1o6  5906  fo1st  6309  fo2nd  6310  tposfo2  6419  ctssdc  7288  exmidfodomrlemim  7387  reeff1o  15455