Theorem f1rnen

Description: Equinumerosity of the range of an injective function. (Contributed by Thierry Arnoux, 7-Jul-2023)

	Ref	Expression
Assertion	f1rnen	|- ( ( F : A -1-1-> B /\ A e. V ) -> ran F ~~ A )

Proof

Step	Hyp	Ref	Expression
1		f1fn	|- ( F : A -1-1-> B -> F Fn A )
2	1	adantr	|- ( ( F : A -1-1-> B /\ A e. V ) -> F Fn A )
3		fnima	|- ( F Fn A -> ( F " A ) = ran F )
4	2 3	syl	|- ( ( F : A -1-1-> B /\ A e. V ) -> ( F " A ) = ran F )
5		ssid	|- A C_ A
6		f1imaeng	|- ( ( F : A -1-1-> B /\ A C_ A /\ A e. V ) -> ( F " A ) ~~ A )
7	5 6	mp3an2	|- ( ( F : A -1-1-> B /\ A e. V ) -> ( F " A ) ~~ A )
8	4 7	eqbrtrrd	|- ( ( F : A -1-1-> B /\ A e. V ) -> ran F ~~ A )