Theorem har2o

Description: The least cardinal greater than 2 is 3. (Contributed by RP, 5-Nov-2023)

	Ref	Expression
Assertion	har2o	⊢ ( har ‘ 2o ) = 3o

Proof

Step	Hyp	Ref	Expression
1		2onn	⊢ 2o ∈ ω
2		harsucnn	⊢ ( 2o ∈ ω → ( har ‘ 2o ) = suc 2o )
3	1 2	ax-mp	⊢ ( har ‘ 2o ) = suc 2o
4		df-3o	⊢ 3o = suc 2o
5	3 4	eqtr4i	⊢ ( har ‘ 2o ) = 3o