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

Metamath Proof Explorer

Theorem fin1a2lem2

Description: Lemma for fin1a2 . The successor operation on the ordinal numbers is injective or one-to-one. Lemma 1.17 of Schloeder p. 2. (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 onsuc 
 |-  ( 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