Definition df-fo 4989

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

This definition is referenced by:  foeq1  5194  foeq2  5195  foeq3  5196  nffo  5197  fof  5198  forn  5201  dffo2  5202  dffn4  5204  fores  5207  dff1o2  5223  dff1o3  5224  foimacnv  5236  foun  5237  fconstfvm  5478  dff1o6  5518  fo1st  5887  fo2nd  5888  tposfo2  5988  exmidfodomrlemim  6774