This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵 ) )

Proof

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