Definition df-fo 5193

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 5185	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5182	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4604	. . . 4 class ran 𝐹
7	6, 2	wceq 1343	. . 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  5405  foeq2  5406  foeq3  5407  nffo  5408  fof  5409  forn  5412  dffo2  5413  dffn4  5415  fores  5418  dff1o2  5436  dff1o3  5437  foimacnv  5449  foun  5450  fconstfvm  5702  dff1o6  5743  fo1st  6122  fo2nd  6123  tposfo2  6231  ctssdc  7074  exmidfodomrlemim  7153  reeff1o  13294