This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rneqdmfinf1o

Description: Any function from a finite set onto the same set must be a bijection. (Contributed by AV, 5-Jul-2021)

Ref Expression
Assertion rneqdmfinf1o 
|- ( ( A e. Fin /\ F Fn A /\ ran F = A ) -> F : A -1-1-onto-> A )

Proof

Step Hyp Ref Expression
1 dffn4 
 |-  ( F Fn A <-> F : A -onto-> ran F )
2 1 biimpi 
 |-  ( F Fn A -> F : A -onto-> ran F )
3 2 3ad2ant2 
 |-  ( ( A e. Fin /\ F Fn A /\ ran F = A ) -> F : A -onto-> ran F )
4 foeq3 
 |-  ( ran F = A -> ( F : A -onto-> ran F <-> F : A -onto-> A ) )
5 4 3ad2ant3 
 |-  ( ( A e. Fin /\ F Fn A /\ ran F = A ) -> ( F : A -onto-> ran F <-> F : A -onto-> A ) )
6 3 5 mpbid 
 |-  ( ( A e. Fin /\ F Fn A /\ ran F = A ) -> F : A -onto-> A )
7 enrefg 
 |-  ( A e. Fin -> A ~~ A )
8 7 3ad2ant1 
 |-  ( ( A e. Fin /\ F Fn A /\ ran F = A ) -> A ~~ A )
9 simp1 
 |-  ( ( A e. Fin /\ F Fn A /\ ran F = A ) -> A e. Fin )
10 fofinf1o 
 |-  ( ( F : A -onto-> A /\ A ~~ A /\ A e. Fin ) -> F : A -1-1-onto-> A )
11 6 8 9 10 syl3anc 
 |-  ( ( A e. Fin /\ F Fn A /\ ran F = A ) -> F : A -1-1-onto-> A )