Definition df-fo 5282

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 5274	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5271	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4680	. . . 4 class ran 𝐹
7	6, 2	wceq 1373	. . 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  5501  foeq2  5502  foeq3  5503  nffo  5504  fof  5505  forn  5508  dffo2  5509  dffn4  5511  fores  5515  dff1o2  5534  dff1o3  5535  foimacnv  5547  foun  5548  fconstfvm  5809  dff1o6  5852  fo1st  6250  fo2nd  6251  tposfo2  6360  ctssdc  7222  exmidfodomrlemim  7316  reeff1o  15289