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