Definition df-fo 5204

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 5196	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5193	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4612	. . . 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  5416  foeq2  5417  foeq3  5418  nffo  5419  fof  5420  forn  5423  dffo2  5424  dffn4  5426  fores  5429  dff1o2  5447  dff1o3  5448  foimacnv  5460  foun  5461  fconstfvm  5714  dff1o6  5755  fo1st  6136  fo2nd  6137  tposfo2  6246  ctssdc  7090  exmidfodomrlemim  7178  reeff1o  13488