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

Metamath Proof Explorer

Theorem suc11

Description: The successor operation behaves like a one-to-one function. Compare Exercise 16 of Enderton p. 194. (Contributed by NM, 3-Sep-2003)

Ref Expression
Assertion suc11 
|- ( ( A e. On /\ B e. On ) -> ( suc A = suc B <-> A = B ) )

Proof

Step Hyp Ref Expression
1 eloni 
 |-  ( A e. On -> Ord A )
2 ordn2lp 
 |-  ( Ord A -> -. ( A e. B /\ B e. A ) )
3 pm3.13 
 |-  ( -. ( A e. B /\ B e. A ) -> ( -. A e. B \/ -. B e. A ) )
4 1 2 3 3syl 
 |-  ( A e. On -> ( -. A e. B \/ -. B e. A ) )
5 4 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( -. A e. B \/ -. B e. A ) )
6 eqimss 
 |-  ( suc A = suc B -> suc A C_ suc B )
7 sucssel 
 |-  ( A e. On -> ( suc A C_ suc B -> A e. suc B ) )
8 6 7 syl5 
 |-  ( A e. On -> ( suc A = suc B -> A e. suc B ) )
9 elsuci 
 |-  ( A e. suc B -> ( A e. B \/ A = B ) )
10 9 ord 
 |-  ( A e. suc B -> ( -. A e. B -> A = B ) )
11 10 com12 
 |-  ( -. A e. B -> ( A e. suc B -> A = B ) )
12 8 11 syl9 
 |-  ( A e. On -> ( -. A e. B -> ( suc A = suc B -> A = B ) ) )
13 eqimss2 
 |-  ( suc A = suc B -> suc B C_ suc A )
14 sucssel 
 |-  ( B e. On -> ( suc B C_ suc A -> B e. suc A ) )
15 13 14 syl5 
 |-  ( B e. On -> ( suc A = suc B -> B e. suc A ) )
16 elsuci 
 |-  ( B e. suc A -> ( B e. A \/ B = A ) )
17 16 ord 
 |-  ( B e. suc A -> ( -. B e. A -> B = A ) )
18 eqcom 
 |-  ( B = A <-> A = B )
19 17 18 imbitrdi 
 |-  ( B e. suc A -> ( -. B e. A -> A = B ) )
20 19 com12 
 |-  ( -. B e. A -> ( B e. suc A -> A = B ) )
21 15 20 syl9 
 |-  ( B e. On -> ( -. B e. A -> ( suc A = suc B -> A = B ) ) )
22 12 21 jaao 
 |-  ( ( A e. On /\ B e. On ) -> ( ( -. A e. B \/ -. B e. A ) -> ( suc A = suc B -> A = B ) ) )
23 5 22 mpd 
 |-  ( ( A e. On /\ B e. On ) -> ( suc A = suc B -> A = B ) )
24 suceq 
 |-  ( A = B -> suc A = suc B )
25 23 24 impbid1 
 |-  ( ( A e. On /\ B e. On ) -> ( suc A = suc B <-> A = B ) )