Theorem suc11reg 3456

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.

Assertion

Ref	Expression
suc11reg	|- (suc A = suc B <-> A = B)

Proof of Theorem suc11reg

Step	Hyp	Ref	Expression
1		en2lp 3453	. . . . 5 |- -. (A e. B /\ B e. A)
2		ianor 253	. . . . 5 |- (-. (A e. B /\ B e. A) <-> (-. A e. B \/ -. B e. A))
3	1, 2	mpbi 164	. . . 4 |- (-. A e. B \/ -. B e. A)
4		eleq2 1150	. . . . . . . . . . . 12 |- (suc A = suc B -> (A e. suc A <-> A e. suc B))
5		sucidg 2305	. . . . . . . . . . . 12 |- (A e. V -> A e. suc A)
6	4, 5	syl5bi 183	. . . . . . . . . . 11 |- (suc A = suc B -> (A e. V -> A e. suc B))
7	6	com12 13	. . . . . . . . . 10 |- (A e. V -> (suc A = suc B -> A e. suc B))
8		elsucg 2290	. . . . . . . . . 10 |- (A e. V -> (A e. suc B <-> (A e. B \/ A = B)))
9	7, 8	sylibd 177	. . . . . . . . 9 |- (A e. V -> (suc A = suc B -> (A e. B \/ A = B)))
10	9	imp 277	. . . . . . . 8 |- ((A e. V /\ suc A = suc B) -> (A e. B \/ A = B))
11	10	ord 202	. . . . . . 7 |- ((A e. V /\ suc A = suc B) -> (-. A e. B -> A = B))
12	11	exp 291	. . . . . 6 |- (A e. V -> (suc A = suc B -> (-. A e. B -> A = B)))
13	12	com23 32	. . . . 5 |- (A e. V -> (-. A e. B -> (suc A = suc B -> A = B)))
14		eleq2 1150	. . . . . . . . . . . . 13 |- (suc A = suc B -> (B e. suc A <-> B e. suc B))
15		sucidg 2305	. . . . . . . . . . . . 13 |- (B e. V -> B e. suc B)
16	14, 15	syl5bir 184	. . . . . . . . . . . 12 |- (suc A = suc B -> (B e. V -> B e. suc A))
17	16	com12 13	. . . . . . . . . . 11 |- (B e. V -> (suc A = suc B -> B e. suc A))
18		elsucg 2290	. . . . . . . . . . 11 |- (B e. V -> (B e. suc A <-> (B e. A \/ B = A)))
19	17, 18	sylibd 177	. . . . . . . . . 10 |- (B e. V -> (suc A = suc B -> (B e. A \/ B = A)))
20	19	imp 277	. . . . . . . . 9 |- ((B e. V /\ suc A = suc B) -> (B e. A \/ B = A))
21	20	ord 202	. . . . . . . 8 |- ((B e. V /\ suc A = suc B) -> (-. B e. A -> B = A))
22		cleqcom 1103	. . . . . . . 8 |- (B = A <-> A = B)
23	21, 22	syl6ib 185	. . . . . . 7 |- ((B e. V /\ suc A = suc B) -> (-. B e. A -> A = B))
24	23	exp 291	. . . . . 6 |- (B e. V -> (suc A = suc B -> (-. B e. A -> A = B)))
25	24	com23 32	. . . . 5 |- (B e. V -> (-. B e. A -> (suc A = suc B -> A = B)))
26	13, 25	jaao 330	. . . 4 |- ((A e. V /\ B e. V) -> ((-. A e. B \/ -. B e. A) -> (suc A = suc B -> A = B)))
27	3, 26	mpi 44	. . 3 |- ((A e. V /\ B e. V) -> (suc A = suc B -> A = B))
28		clneq 1168	. . . . 5 |- ((suc A e. V /\ -. suc B e. V) -> -. suc A = suc B)
29		sucexb 2301	. . . . 5 |- (A e. V <-> suc A e. V)
30		sucexb 2301	. . . . . 6 |- (B e. V <-> suc B e. V)
31	30	negbii 162	. . . . 5 |- (-. B e. V <-> -. suc B e. V)
32	28, 29, 31	syl2anb 350	. . . 4 |- ((A e. V /\ -. B e. V) -> -. suc A = suc B)
33	32	pm2.21d 74	. . 3 |- ((A e. V /\ -. B e. V) -> (suc A = suc B -> A = B))
34		clneq 1168	. . . . . . 7 |- ((suc B e. V /\ -. suc A e. V) -> -. suc B = suc A)
35	29	negbii 162	. . . . . . 7 |- (-. A e. V <-> -. suc A e. V)
36	34, 30, 35	syl2anb 350	. . . . . 6 |- ((B e. V /\ -. A e. V) -> -. suc B = suc A)
37	36	ancoms 334	. . . . 5 |- ((-. A e. V /\ B e. V) -> -. suc B = suc A)
38	37	pm2.21d 74	. . . 4 |- ((-. A e. V /\ B e. V) -> (suc B = suc A -> A = B))
39		cleqcom 1103	. . . 4 |- (suc A = suc B <-> suc B = suc A)
40	38, 39	syl5ib 181	. . 3 |- ((-. A e. V /\ B e. V) -> (suc A = suc B -> A = B))
41		sucprc 2297	. . . . 5 |- (-. A e. V -> suc A = A)
42		sucprc 2297	. . . . 5 |- (-. B e. V -> suc B = B)
43	41, 42	cleqan12d 1116	. . . 4 |- ((-. A e. V /\ -. B e. V) -> (suc A = suc B <-> A = B))
44	43	biimpd 135	. . 3 |- ((-. A e. V /\ -. B e. V) -> (suc A = suc B -> A = B))
45	27, 33, 40, 44	4cases 565	. 2 |- (suc A = suc B -> A = B)
46		suceq 2288	. 2 |- (A = B -> suc A = suc B)
47	45, 46	impbi 139	1 |- (suc A = suc B <-> A = B)

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   \/ wo 195   /\ wa 196   = wceq 1091   e. wcel 1092  Vcvv 1348  suc csuc 2201

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-eprel 2122  df-fr 2169  df-suc 2205

metamath.org