Definition df-fo 4851

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	⊢ (𝐹:A–onto→B ↔ (𝐹 Fn A ∧ ran 𝐹 = B))

Detailed syntax breakdown of Definition df-fo

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class 𝐹
4	1, 2, 3	wfo 4843	. 2 wff 𝐹:A–onto→B
5	3, 1	wfn 4840	. . 3 wff 𝐹 Fn A
6	3	crn 4289	. . . 4 class ran 𝐹
7	6, 2	wceq 1242	. . 3 wff ran 𝐹 = B
8	5, 7	wa 97	. 2 wff (𝐹 Fn A ∧ ran 𝐹 = B)
9	4, 8	wb 98	1 wff (𝐹:A–onto→B ↔ (𝐹 Fn A ∧ ran 𝐹 = B))

This definition is referenced by:  foeq1  5045  foeq2  5046  foeq3  5047  nffo  5048  fof  5049  forn  5052  dffo2  5053  dffn4  5055  fores  5058  dff1o2  5074  dff1o3  5075  foimacnv  5087  foun  5088  fconstfvm  5322  dff1o6  5359  fo1st  5726  fo2nd  5727  tposfo2  5823