Theorem suc11g 4302

Description: The successor operation behaves like a one-to-one function (assuming the Axiom of Set Induction). Similar to Exercise 35 of [Enderton] p. 208 and its converse. (Contributed by NM, 25-Oct-2003.)

Assertion

Ref	Expression
suc11g	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵))

Proof of Theorem suc11g

Step	Hyp	Ref	Expression
1		en2lp 4299	. . . 4 ⊢ ¬ (𝐵 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵)
2		sucidg 4173	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ suc 𝐵)
3		eleq2 2143	. . . . . . . . . . . 12 ⊢ (suc 𝐴 = suc 𝐵 → (𝐵 ∈ suc 𝐴 ↔ 𝐵 ∈ suc 𝐵))
4	2, 3	syl5ibrcom 155	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑊 → (suc 𝐴 = suc 𝐵 → 𝐵 ∈ suc 𝐴))
5		elsucg 4161	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑊 → (𝐵 ∈ suc 𝐴 ↔ (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴)))
6	4, 5	sylibd 147	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑊 → (suc 𝐴 = suc 𝐵 → (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴)))
7	6	imp 122	. . . . . . . . 9 ⊢ ((𝐵 ∈ 𝑊 ∧ suc 𝐴 = suc 𝐵) → (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴))
8	7	3adant1 957	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ suc 𝐴 = suc 𝐵) → (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴))
9		sucidg 4173	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)
10		eleq2 2143	. . . . . . . . . . . 12 ⊢ (suc 𝐴 = suc 𝐵 → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ suc 𝐵))
11	9, 10	syl5ibcom 153	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑉 → (suc 𝐴 = suc 𝐵 → 𝐴 ∈ suc 𝐵))
12		elsucg 4161	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
13	11, 12	sylibd 147	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → (suc 𝐴 = suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
14	13	imp 122	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ suc 𝐴 = suc 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
15	14	3adant2 958	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ suc 𝐴 = suc 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
16	8, 15	jca 300	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ suc 𝐴 = suc 𝐵) → ((𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴) ∧ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
17		eqcom 2084	. . . . . . . . 9 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵)
18	17	orbi2i 712	. . . . . . . 8 ⊢ ((𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴) ↔ (𝐵 ∈ 𝐴 ∨ 𝐴 = 𝐵))
19	18	anbi1i 446	. . . . . . 7 ⊢ (((𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴) ∧ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) ↔ ((𝐵 ∈ 𝐴 ∨ 𝐴 = 𝐵) ∧ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
20	16, 19	sylib 120	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ suc 𝐴 = suc 𝐵) → ((𝐵 ∈ 𝐴 ∨ 𝐴 = 𝐵) ∧ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
21		ordir 764	. . . . . 6 ⊢ (((𝐵 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) ∨ 𝐴 = 𝐵) ↔ ((𝐵 ∈ 𝐴 ∨ 𝐴 = 𝐵) ∧ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
22	20, 21	sylibr 132	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ suc 𝐴 = suc 𝐵) → ((𝐵 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) ∨ 𝐴 = 𝐵))
23	22	ord 676	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ suc 𝐴 = suc 𝐵) → (¬ (𝐵 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐴 = 𝐵))
24	1, 23	mpi 15	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ suc 𝐴 = suc 𝐵) → 𝐴 = 𝐵)
25	24	3expia 1141	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵))
26		suceq 4159	. 2 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)
27	25, 26	impbid1 140	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 102   ↔ wb 103   ∨ wo 662   ∧ w3a 920   = wceq 1285   ∈ wcel 1434  suc csuc 4122

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-setind 4282

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-v 2604  df-dif 2976  df-un 2978  df-sn 3406  df-pr 3407  df-suc 4128

This theorem is referenced by:  suc11  4303  peano4  4340  frecsuclem  6049