Definition df-fo 5260

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 5252	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5249	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4660	. . . 4 class ran 𝐹
7	6, 2	wceq 1364	. . 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  5472  foeq2  5473  foeq3  5474  nffo  5475  fof  5476  forn  5479  dffo2  5480  dffn4  5482  fores  5486  dff1o2  5505  dff1o3  5506  foimacnv  5518  foun  5519  fconstfvm  5776  dff1o6  5819  fo1st  6210  fo2nd  6211  tposfo2  6320  ctssdc  7172  exmidfodomrlemim  7261  reeff1o  14908