Metamath Proof Explorer

Theorem hash4

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

Ref Expression
Assertion hash4 
|- ( # ` 4o ) = 4

Proof

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