Definition df-fo 5264

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 5256	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5253	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4664	. . . 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  5476  foeq2  5477  foeq3  5478  nffo  5479  fof  5480  forn  5483  dffo2  5484  dffn4  5486  fores  5490  dff1o2  5509  dff1o3  5510  foimacnv  5522  foun  5523  fconstfvm  5780  dff1o6  5823  fo1st  6215  fo2nd  6216  tposfo2  6325  ctssdc  7179  exmidfodomrlemim  7268  reeff1o  15009