Metamath Proof Explorer

Theorem hash2

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

Ref Expression
Assertion hash2 
|- ( # ` 2o ) = 2

Proof

Step Hyp Ref Expression
1 1onn 
 |-  1o e. _om
2 df-2o 
 |-  2o = suc 1o
3 hash1 
 |-  ( # ` 1o ) = 1
4 1p1e2 
 |-  ( 1 + 1 ) = 2
5 1 2 3 4 hashp1i 
 |-  ( # ` 2o ) = 2