Definition df-fo 5202

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 5194	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5191	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4610	. . . 4 class ran 𝐹
7	6, 2	wceq 1348	. . 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  5414  foeq2  5415  foeq3  5416  nffo  5417  fof  5418  forn  5421  dffo2  5422  dffn4  5424  fores  5427  dff1o2  5445  dff1o3  5446  foimacnv  5458  foun  5459  fconstfvm  5711  dff1o6  5752  fo1st  6133  fo2nd  6134  tposfo2  6243  ctssdc  7086  exmidfodomrlemim  7165  reeff1o  13447