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 syl6ib
 |-  ( 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 ) )