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 syl6ib ⊢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