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	syl6ib	|- ( ( 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	syl5bi	|- ( ( -. 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 )