Metamath Proof Explorer


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