Theorem fin1a2lem2

Description: Lemma for fin1a2 . (Contributed by Stefan O'Rear, 7-Nov-2014)

	Ref	Expression
Hypothesis	fin1a2lem.a	|- S = ( x e. On |-> suc x )
Assertion	fin1a2lem2	|- S : On -1-1-> On

Proof

Step	Hyp	Ref	Expression
1		fin1a2lem.a	|- S = ( x e. On |-> suc x )
2		suceloni	|- ( x e. On -> suc x e. On )
3	1 2	fmpti	|- S : On --> On
4	1	fin1a2lem1	|- ( a e. On -> ( S ` a ) = suc a )
5	1	fin1a2lem1	|- ( b e. On -> ( S ` b ) = suc b )
6	4 5	eqeqan12d	|- ( ( a e. On /\ b e. On ) -> ( ( S ` a ) = ( S ` b ) <-> suc a = suc b ) )
7		suc11	|- ( ( a e. On /\ b e. On ) -> ( suc a = suc b <-> a = b ) )
8	6 7	bitrd	|- ( ( a e. On /\ b e. On ) -> ( ( S ` a ) = ( S ` b ) <-> a = b ) )
9	8	biimpd	|- ( ( a e. On /\ b e. On ) -> ( ( S ` a ) = ( S ` b ) -> a = b ) )
10	9	rgen2	|- A. a e. On A. b e. On ( ( S ` a ) = ( S ` b ) -> a = b )
11		dff13	|- ( S : On -1-1-> On <-> ( S : On --> On /\ A. a e. On A. b e. On ( ( S ` a ) = ( S ` b ) -> a = b ) ) )
12	3 10 11	mpbir2an	|- S : On -1-1-> On