Definition df-fo 5332

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 5324	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5321	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4726	. . . 4 class ran 𝐹
7	6, 2	wceq 1397	. . 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  5555  foeq2  5556  foeq3  5557  nffo  5558  fof  5559  forn  5562  dffo2  5563  dffn4  5565  fores  5569  dff1o2  5588  dff1o3  5589  foimacnv  5601  foun  5602  fconstfvm  5871  dff1o6  5916  fo1st  6319  fo2nd  6320  tposfo2  6432  ctssdc  7311  exmidfodomrlemim  7411  reeff1o  15496