Metamath Proof Explorer

Theorem suc11

Description: The successor operation behaves like a one-to-one function. Compare Exercise 16 of Enderton p. 194. (Contributed by NM, 3-Sep-2003)

Ref Expression
Assertion suc11 ⊢ A ∈ On ∧ B ∈ On → suc ⁡ A = suc ⁡ B ↔ A = B

Proof

Step Hyp Ref Expression
1 eloni ⊢ A ∈ On → Ord ⁡ A
2 ordn2lp ⊢ Ord ⁡ A → ¬ A ∈ B ∧ B ∈ A
3 pm3.13 ⊢ ¬ A ∈ B ∧ B ∈ A → ¬ A ∈ B ∨ ¬ B ∈ A
4 1 2 3 3syl ⊢ A ∈ On → ¬ A ∈ B ∨ ¬ B ∈ A
5 4 adantr ⊢ A ∈ On ∧ B ∈ On → ¬ A ∈ B ∨ ¬ B ∈ A
6 eqimss ⊢ suc ⁡ A = suc ⁡ B → suc ⁡ A ⊆ suc ⁡ B
7 sucssel ⊢ A ∈ On → suc ⁡ A ⊆ suc ⁡ B → A ∈ suc ⁡ B
8 6 7 syl5 ⊢ A ∈ On → suc ⁡ A = suc ⁡ B → A ∈ suc ⁡ B
9 elsuci ⊢ A ∈ suc ⁡ B → A ∈ B ∨ A = B
10 9 ord ⊢ A ∈ suc ⁡ B → ¬ A ∈ B → A = B
11 10 com12 ⊢ ¬ A ∈ B → A ∈ suc ⁡ B → A = B
12 8 11 syl9 ⊢ A ∈ On → ¬ A ∈ B → suc ⁡ A = suc ⁡ B → A = B
13 eqimss2 ⊢ suc ⁡ A = suc ⁡ B → suc ⁡ B ⊆ suc ⁡ A
14 sucssel ⊢ B ∈ On → suc ⁡ B ⊆ suc ⁡ A → B ∈ suc ⁡ A
15 13 14 syl5 ⊢ B ∈ On → suc ⁡ A = suc ⁡ B → B ∈ suc ⁡ A
16 elsuci ⊢ B ∈ suc ⁡ A → B ∈ A ∨ B = A
17 16 ord ⊢ B ∈ suc ⁡ A → ¬ B ∈ A → B = A
18 eqcom ⊢ B = A ↔ A = B
19 17 18 imbitrdi ⊢ B ∈ suc ⁡ A → ¬ B ∈ A → A = B
20 19 com12 ⊢ ¬ B ∈ A → B ∈ suc ⁡ A → A = B
21 15 20 syl9 ⊢ B ∈ On → ¬ B ∈ A → suc ⁡ A = suc ⁡ B → A = B
22 12 21 jaao ⊢ A ∈ On ∧ B ∈ On → ¬ A ∈ B ∨ ¬ B ∈ A → suc ⁡ A = suc ⁡ B → A = B
23 5 22 mpd ⊢ A ∈ On ∧ B ∈ On → suc ⁡ A = suc ⁡ B → A = B
24 suceq ⊢ A = B → suc ⁡ A = suc ⁡ B
25 23 24 impbid1 ⊢ A ∈ On ∧ B ∈ On → suc ⁡ A = suc ⁡ B ↔ A = B