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