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

Metamath Proof Explorer

Theorem cardsucnn

Description: The cardinality of the successor of a finite ordinal (natural number). This theorem does not hold for infinite ordinals; see cardsucinf . (Contributed by NM, 7-Nov-2008)

Ref Expression
Assertion cardsucnn ⊢ A ∈ ω → card ⁡ suc ⁡ A = suc ⁡ card ⁡ A

Proof

Step Hyp Ref Expression
1 peano2 ⊢ A ∈ ω → suc ⁡ A ∈ ω
2 cardnn ⊢ suc ⁡ A ∈ ω → card ⁡ suc ⁡ A = suc ⁡ A
3 1 2 syl ⊢ A ∈ ω → card ⁡ suc ⁡ A = suc ⁡ A
4 cardnn ⊢ A ∈ ω → card ⁡ A = A
5 suceq ⊢ card ⁡ A = A → suc ⁡ card ⁡ A = suc ⁡ A
6 4 5 syl ⊢ A ∈ ω → suc ⁡ card ⁡ A = suc ⁡ A
7 3 6 eqtr4d ⊢ A ∈ ω → card ⁡ suc ⁡ A = suc ⁡ card ⁡ A