Description: Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | hash1 | ⊢ ( ♯ ‘ 1o ) = 1 |
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 |