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 \leftrightarrow A = B$

Proof

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

Metamath Proof Explorer

Theorem suc11reg

Proof