Metamath Proof Explorer


Theorem hash4

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

Ref Expression
Assertion hash4 4𝑜=4

Proof

Step Hyp Ref Expression
1 3onn 3𝑜ω
2 df-4o 4𝑜=suc3𝑜
3 hash3 3𝑜=3
4 3p1e4 3+1=4
5 1 2 3 4 hashp1i 4𝑜=4