Definition df-fo 5360

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 5352	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5349	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4752	. . . 4 class ran 𝐹
7	6, 2	wceq 1398	. . 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  5588  foeq2  5589  foeq3  5590  nffo  5591  fof  5592  forn  5595  dffo2  5596  dffn4  5598  fores  5602  dff1o2  5621  dff1o3  5622  foimacnv  5634  foun  5635  fconstfvm  5904  dff1o6  5951  fo1st  6353  fo2nd  6354  tposfo2  6500  ctssdc  7406  exmidfodomrlemim  7506  reeff1o  15655