Definition df-fo 5137

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 5129	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5126	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4548	. . . 4 class ran 𝐹
7	6, 2	wceq 1332	. . 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  5349  foeq2  5350  foeq3  5351  nffo  5352  fof  5353  forn  5356  dffo2  5357  dffn4  5359  fores  5362  dff1o2  5380  dff1o3  5381  foimacnv  5393  foun  5394  fconstfvm  5646  dff1o6  5685  fo1st  6063  fo2nd  6064  tposfo2  6172  ctssdc  7006  exmidfodomrlemim  7074  reeff1o  12902