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  5872  dff1o6  5917  fo1st  6320  fo2nd  6321  tposfo2  6433  ctssdc  7312  exmidfodomrlemim  7412  reeff1o  15516