Definition df-fo 4928

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

This definition is referenced by:  foeq1  5122  foeq2  5123  foeq3  5124  nffo  5125  fof  5126  forn  5129  dffo2  5130  dffn4  5132  fores  5135  dff1o2  5151  dff1o3  5152  foimacnv  5164  foun  5165  fconstfvm  5400  dff1o6  5436  fo1st  5804  fo2nd  5805  tposfo2  5905