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	⊢ ∅ ∈ ω
2		df-1o	⊢ 1o = suc ∅
3		hash0	⊢ ( ♯ ‘ ∅ ) = 0
4		0p1e1	⊢ ( 0 + 1 ) = 1
5	1 2 3 4	hashp1i	⊢ ( ♯ ‘ 1o ) = 1