Definition df-fo 5363

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 5355	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5352	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4755	. . . 4 class ran 𝐹
7	6, 2	wceq 1398	. . 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  5591  foeq2  5592  foeq3  5593  nffo  5594  fof  5595  forn  5598  dffo2  5599  dffn4  5601  fores  5605  dff1o2  5624  dff1o3  5625  foimacnv  5637  foun  5638  fconstfvm  5907  dff1o6  5955  fo1st  6364  fo2nd  6365  tposfo2  6511  ctssdc  7417  exmidfodomrlemim  7517  reeff1o  15764