Definition df-fo 5386

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 5378	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5375	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4777	. . . 4 class ran 𝐹
7	6, 2	wceq 1402	. . 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 used by:  foeq1  5614  foeq2  5615  foeq3  5616  nffo  5617  fof  5618  forn  5621  dffo2  5622  dffn4  5624  fores  5628  dff1o2  5647  dff1o3  5648  foimacnv  5660  foun  5661  fconstfvm  5936  dff1o6  5985  fo1st  6395  fo2nd  6396  tposfo2  6542  ctssdc  7459  exmidfodomrlemim  7559  reeff1o  15999