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

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 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵 )

Proof

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