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 A = suc B <-> A = B )

Proof

Step Hyp Ref Expression
1 en2lp 
 |-  -. ( A e. B /\ B e. A )
2 ianor 
 |-  ( -. ( A e. B /\ B e. A ) <-> ( -. A e. B \/ -. B e. A ) )
3 1 2 mpbi 
 |-  ( -. A e. B \/ -. B e. A )
4 sucidg 
 |-  ( A e. _V -> A e. suc A )
5 eleq2 
 |-  ( suc A = suc B -> ( A e. suc A <-> A e. suc B ) )
6 4 5 syl5ibcom 
 |-  ( A e. _V -> ( suc A = suc B -> A e. suc B ) )
7 elsucg 
 |-  ( A e. _V -> ( A e. suc B <-> ( A e. B \/ A = B ) ) )
8 6 7 sylibd 
 |-  ( A e. _V -> ( suc A = suc B -> ( A e. B \/ A = B ) ) )
9 8 imp 
 |-  ( ( A e. _V /\ suc A = suc B ) -> ( A e. B \/ A = B ) )
10 9 ord 
 |-  ( ( A e. _V /\ suc A = suc B ) -> ( -. A e. B -> A = B ) )
11 10 ex 
 |-  ( A e. _V -> ( suc A = suc B -> ( -. A e. B -> A = B ) ) )
12 11 com23 
 |-  ( A e. _V -> ( -. A e. B -> ( suc A = suc B -> A = B ) ) )
13 sucidg 
 |-  ( B e. _V -> B e. suc B )
14 eleq2 
 |-  ( suc A = suc B -> ( B e. suc A <-> B e. suc B ) )
15 13 14 syl5ibrcom 
 |-  ( B e. _V -> ( suc A = suc B -> B e. suc A ) )
16 elsucg 
 |-  ( B e. _V -> ( B e. suc A <-> ( B e. A \/ B = A ) ) )
17 15 16 sylibd 
 |-  ( B e. _V -> ( suc A = suc B -> ( B e. A \/ B = A ) ) )
18 17 imp 
 |-  ( ( B e. _V /\ suc A = suc B ) -> ( B e. A \/ B = A ) )
19 18 ord 
 |-  ( ( B e. _V /\ suc A = suc B ) -> ( -. B e. A -> B = A ) )
20 eqcom 
 |-  ( B = A <-> A = B )
21 19 20 imbitrdi 
 |-  ( ( B e. _V /\ suc A = suc B ) -> ( -. B e. A -> A = B ) )
22 21 ex 
 |-  ( B e. _V -> ( suc A = suc B -> ( -. B e. A -> A = B ) ) )
23 22 com23 
 |-  ( B e. _V -> ( -. B e. A -> ( suc A = suc B -> A = B ) ) )
24 12 23 jaao 
 |-  ( ( A e. _V /\ B e. _V ) -> ( ( -. A e. B \/ -. B e. A ) -> ( suc A = suc B -> A = B ) ) )
25 3 24 mpi 
 |-  ( ( A e. _V /\ B e. _V ) -> ( suc A = suc B -> A = B ) )
26 sucexb 
 |-  ( A e. _V <-> suc A e. _V )
27 sucexb 
 |-  ( B e. _V <-> suc B e. _V )
28 27 notbii 
 |-  ( -. B e. _V <-> -. suc B e. _V )
29 nelneq 
 |-  ( ( suc A e. _V /\ -. suc B e. _V ) -> -. suc A = suc B )
30 26 28 29 syl2anb 
 |-  ( ( A e. _V /\ -. B e. _V ) -> -. suc A = suc B )
31 30 pm2.21d 
 |-  ( ( A e. _V /\ -. B e. _V ) -> ( suc A = suc B -> A = B ) )
32 eqcom 
 |-  ( suc A = suc B <-> suc B = suc A )
33 26 notbii 
 |-  ( -. A e. _V <-> -. suc A e. _V )
34 nelneq 
 |-  ( ( suc B e. _V /\ -. suc A e. _V ) -> -. suc B = suc A )
35 27 33 34 syl2anb 
 |-  ( ( B e. _V /\ -. A e. _V ) -> -. suc B = suc A )
36 35 ancoms 
 |-  ( ( -. A e. _V /\ B e. _V ) -> -. suc B = suc A )
37 36 pm2.21d 
 |-  ( ( -. A e. _V /\ B e. _V ) -> ( suc B = suc A -> A = B ) )
38 32 37 biimtrid 
 |-  ( ( -. A e. _V /\ B e. _V ) -> ( suc A = suc B -> A = B ) )
39 sucprc 
 |-  ( -. A e. _V -> suc A = A )
40 sucprc 
 |-  ( -. B e. _V -> suc B = B )
41 39 40 eqeqan12d 
 |-  ( ( -. A e. _V /\ -. B e. _V ) -> ( suc A = suc B <-> A = B ) )
42 41 biimpd 
 |-  ( ( -. A e. _V /\ -. B e. _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 )