Theorem hash3

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

	Ref	Expression
Assertion	hash3	⊢ ( ♯ ‘ 3o ) = 3

Proof

Step	Hyp	Ref	Expression
1		2onn	⊢ 2o ∈ ω
2		df-3o	⊢ 3o = suc 2o
3		hash2	⊢ ( ♯ ‘ 2o ) = 2
4		2p1e3	⊢ ( 2 + 1 ) = 3
5	1 2 3 4	hashp1i	⊢ ( ♯ ‘ 3o ) = 3