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