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