Metamath Proof Explorer


Theorem hash1

Description: Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016)

Ref Expression
Assertion hash1 ( ♯ ‘ 1o ) = 1

Proof

Step Hyp Ref Expression
1 peano1 ∅ ∈ ω
2 df-1o 1o = suc ∅
3 hash0 ( ♯ ‘ ∅ ) = 0
4 0p1e1 ( 0 + 1 ) = 1
5 1 2 3 4 hashp1i ( ♯ ‘ 1o ) = 1