Definition df-fo 5381

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 5373	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5370	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4773	. . . 4 class ran 𝐹
7	6, 2	wceq 1402	. . 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  5609  foeq2  5610  foeq3  5611  nffo  5612  fof  5613  forn  5616  dffo2  5617  dffn4  5619  fores  5623  dff1o2  5642  dff1o3  5643  foimacnv  5655  foun  5656  fconstfvm  5927  dff1o6  5975  fo1st  6384  fo2nd  6385  tposfo2  6531  ctssdc  7446  exmidfodomrlemim  7546  reeff1o  15800