Theorem focdmex

Description: The codomain of an onto function is a set if its domain is a set. (Contributed by AV, 4-May-2021)

	Ref	Expression
Assertion	focdmex	|- ( ( A e. V /\ F : A -onto-> B ) -> B e. _V )

Proof

Step	Hyp	Ref	Expression
1		fof	|- ( F : A -onto-> B -> F : A --> B )
2	1	anim2i	|- ( ( A e. V /\ F : A -onto-> B ) -> ( A e. V /\ F : A --> B ) )
3	2	ancomd	|- ( ( A e. V /\ F : A -onto-> B ) -> ( F : A --> B /\ A e. V ) )
4		fex	|- ( ( F : A --> B /\ A e. V ) -> F e. _V )
5		rnexg	|- ( F e. _V -> ran F e. _V )
6	3 4 5	3syl	|- ( ( A e. V /\ F : A -onto-> B ) -> ran F e. _V )
7		forn	|- ( F : A -onto-> B -> ran F = B )
8	7	eleq1d	|- ( F : A -onto-> B -> ( ran F e. _V <-> B e. _V ) )
9	8	adantl	|- ( ( A e. V /\ F : A -onto-> B ) -> ( ran F e. _V <-> B e. _V ) )
10	6 9	mpbid	|- ( ( A e. V /\ F : A -onto-> B ) -> B e. _V )