Definition df-fo 5328

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 5320	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5317	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4722	. . . 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  5550  foeq2  5551  foeq3  5552  nffo  5553  fof  5554  forn  5557  dffo2  5558  dffn4  5560  fores  5564  dff1o2  5583  dff1o3  5584  foimacnv  5596  foun  5597  fconstfvm  5865  dff1o6  5910  fo1st  6313  fo2nd  6314  tposfo2  6426  ctssdc  7301  exmidfodomrlemim  7400  reeff1o  15484