Definition df-fo 5241

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 5233	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5230	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4645	. . . 4 class ran 𝐹
7	6, 2	wceq 1364	. . 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  5453  foeq2  5454  foeq3  5455  nffo  5456  fof  5457  forn  5460  dffo2  5461  dffn4  5463  fores  5466  dff1o2  5485  dff1o3  5486  foimacnv  5498  foun  5499  fconstfvm  5754  dff1o6  5797  fo1st  6181  fo2nd  6182  tposfo2  6291  ctssdc  7141  exmidfodomrlemim  7229  reeff1o  14646