Definition df-fo 5055

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 5047	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5044	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4468	. . . 4 class ran 𝐹
7	6, 2	wceq 1296	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 103	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 104	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  5264  foeq2  5265  foeq3  5266  nffo  5267  fof  5268  forn  5271  dffo2  5272  dffn4  5274  fores  5277  dff1o2  5293  dff1o3  5294  foimacnv  5306  foun  5307  fconstfvm  5554  dff1o6  5593  fo1st  5966  fo2nd  5967  tposfo2  6070  exmidfodomrlemim  6924