Definition df-fo 4823

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 4815	. 2 wff 𝐹:A–onto→B
5	3, 1	wfn 4812	. . 3 wff 𝐹 Fn A
6	3	crn 4261	. . . 4 class ran 𝐹
7	6, 2	wceq 1223	. . 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  5015  foeq2  5016  foeq3  5017  nffo  5018  fof  5019  forn  5022  dffo2  5023  dffn4  5025  fores  5028  dff1o2  5044  dff1o3  5045  foimacnv  5057  foun  5058  fconstfvm  5292  dff1o6  5329  fo1st  5695  fo2nd  5696  tposfo2  5792