Metamath Proof Explorer


Theorem suc11reg

Description: The successor operation behaves like a one-to-one function (assuming the Axiom of Regularity). Exercise 35 of Enderton p. 208 and its converse. (Contributed by NM, 25-Oct-2003)

Ref Expression
Assertion suc11reg suc A = suc B A = B

Proof

Step Hyp Ref Expression
1 en2lp ¬ A B B A
2 ianor ¬ A B B A ¬ A B ¬ B A
3 1 2 mpbi ¬ A B ¬ B A
4 sucidg A V A suc A
5 eleq2 suc A = suc B A suc A A suc B
6 4 5 syl5ibcom A V suc A = suc B A suc B
7 elsucg A V A suc B A B A = B
8 6 7 sylibd A V suc A = suc B A B A = B
9 8 imp A V suc A = suc B A B A = B
10 9 ord A V suc A = suc B ¬ A B A = B
11 10 ex A V suc A = suc B ¬ A B A = B
12 11 com23 A V ¬ A B suc A = suc B A = B
13 sucidg B V B suc B
14 eleq2 suc A = suc B B suc A B suc B
15 13 14 syl5ibrcom B V suc A = suc B B suc A
16 elsucg B V B suc A B A B = A
17 15 16 sylibd B V suc A = suc B B A B = A
18 17 imp B V suc A = suc B B A B = A
19 18 ord B V suc A = suc B ¬ B A B = A
20 eqcom B = A A = B
21 19 20 syl6ib B V suc A = suc B ¬ B A A = B
22 21 ex B V suc A = suc B ¬ B A A = B
23 22 com23 B V ¬ B A suc A = suc B A = B
24 12 23 jaao A V B V ¬ A B ¬ B A suc A = suc B A = B
25 3 24 mpi A V B V suc A = suc B A = B
26 sucexb A V suc A V
27 sucexb B V suc B V
28 27 notbii ¬ B V ¬ suc B V
29 nelneq suc A V ¬ suc B V ¬ suc A = suc B
30 26 28 29 syl2anb A V ¬ B V ¬ suc A = suc B
31 30 pm2.21d A V ¬ B V suc A = suc B A = B
32 eqcom suc A = suc B suc B = suc A
33 26 notbii ¬ A V ¬ suc A V
34 nelneq suc B V ¬ suc A V ¬ suc B = suc A
35 27 33 34 syl2anb B V ¬ A V ¬ suc B = suc A
36 35 ancoms ¬ A V B V ¬ suc B = suc A
37 36 pm2.21d ¬ A V B V suc B = suc A A = B
38 32 37 syl5bi ¬ A V B V suc A = suc B A = B
39 sucprc ¬ A V suc A = A
40 sucprc ¬ B V suc B = B
41 39 40 eqeqan12d ¬ A V ¬ B V suc A = suc B A = B
42 41 biimpd ¬ A V ¬ B V suc A = suc B A = B
43 25 31 38 42 4cases suc A = suc B A = B
44 suceq A = B suc A = suc B
45 43 44 impbii suc A = suc B A = B