Definition df-fo

Description: Define an onto function. Definition 6.15(4) of TakeutiZaring p. 27. We use their notation ("onto" under the arrow). For alternate definitions, see dffo2 , dffo3 , dffo4 , and dffo5 .

An onto function is also called a "surjection" or a "surjective function", F : A -onto-> B can be read as " F is a surjection from A onto B ". Surjections are precisely the epimorphisms in the category SetCat of sets and set functions, see setcepi . (Contributed by NM, 1-Aug-1994)

	Ref	Expression
Assertion	df-fo	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	⊢ 𝐹
1		cA	⊢ 𝐴
2		cB	⊢ 𝐵
3	1 2 0	wfo	⊢ 𝐹 : 𝐴 –onto→ 𝐵
4	0 1	wfn	⊢ 𝐹 Fn 𝐴
5	0	crn	⊢ ran 𝐹
6	5 2	wceq	⊢ ran 𝐹 = 𝐵
7	4 6	wa	⊢ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 )
8	3 7	wb	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) )