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 
 |-  (/) e. _om
2 df-1o 
 |-  1o = suc (/)
3 hash0 
 |-  ( # ` (/) ) = 0
4 0p1e1 
 |-  ( 0 + 1 ) = 1
5 1 2 3 4 hashp1i 
 |-  ( # ` 1o ) = 1