Definition df-fo 5383

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 5375	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5372	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4775	. . . 4 class ran 𝐹
7	6, 2	wceq 1402	. . 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 used by:  foeq1  5611  foeq2  5612  foeq3  5613  nffo  5614  fof  5615  forn  5618  dffo2  5619  dffn4  5621  fores  5625  dff1o2  5644  dff1o3  5645  foimacnv  5657  foun  5658  fconstfvm  5933  dff1o6  5982  fo1st  6391  fo2nd  6392  tposfo2  6538  ctssdc  7453  exmidfodomrlemim  7553  reeff1o  15874