Definition df-fo 5129

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

This definition is referenced by:  foeq1  5341  foeq2  5342  foeq3  5343  nffo  5344  fof  5345  forn  5348  dffo2  5349  dffn4  5351  fores  5354  dff1o2  5372  dff1o3  5373  foimacnv  5385  foun  5386  fconstfvm  5638  dff1o6  5677  fo1st  6055  fo2nd  6056  tposfo2  6164  ctssdc  6998  exmidfodomrlemim  7057