Theorem f1oexrnex

Description: If the range of a 1-1 onto function is a set, the function itself is a set. (Contributed by AV, 2-Jun-2019)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( F : A -1-1-onto-> B /\ B e. V ) -> F : A -1-1-onto-> B )
2		f1ocnv	|- ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )
3		f1of	|- ( `' F : B -1-1-onto-> A -> `' F : B --> A )
4	1 2 3	3syl	|- ( ( F : A -1-1-onto-> B /\ B e. V ) -> `' F : B --> A )
5		fex	|- ( ( `' F : B --> A /\ B e. V ) -> `' F e. _V )
6	4 5	sylancom	|- ( ( F : A -1-1-onto-> B /\ B e. V ) -> `' F e. _V )
7		f1orel	|- ( F : A -1-1-onto-> B -> Rel F )
8	7	adantr	|- ( ( F : A -1-1-onto-> B /\ B e. V ) -> Rel F )
9		relcnvexb	|- ( Rel F -> ( F e. _V <-> `' F e. _V ) )
10	8 9	syl	|- ( ( F : A -1-1-onto-> B /\ B e. V ) -> ( F e. _V <-> `' F e. _V ) )
11	6 10	mpbird	|- ( ( F : A -1-1-onto-> B /\ B e. V ) -> F e. _V )