Definition df-fo 5300

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 5292	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5289	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4697	. . . 4 class ran 𝐹
7	6, 2	wceq 1375	. . 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  5520  foeq2  5521  foeq3  5522  nffo  5523  fof  5524  forn  5527  dffo2  5528  dffn4  5530  fores  5534  dff1o2  5553  dff1o3  5554  foimacnv  5566  foun  5567  fconstfvm  5830  dff1o6  5873  fo1st  6273  fo2nd  6274  tposfo2  6383  ctssdc  7248  exmidfodomrlemim  7347  reeff1o  15412