Theorem har2o

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

	Ref	Expression
Assertion	har2o	$$⊢\mathrm{har}\left(2_{𝑜}\right)=3_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		2onn	$$⊢2_{𝑜}\in \mathrm{\omega }$$
2		harsucnn	$$⊢2_{𝑜}\in \mathrm{\omega }\to \mathrm{har}\left(2_{𝑜}\right)=\mathrm{suc}{2}_{𝑜}$$
3	1 2	ax-mp	$$⊢\mathrm{har}\left(2_{𝑜}\right)=\mathrm{suc}{2}_{𝑜}$$
4		df-3o	$$⊢3_{𝑜}=\mathrm{suc}{2}_{𝑜}$$
5	3 4	eqtr4i	$$⊢\mathrm{har}\left(2_{𝑜}\right)=3_{𝑜}$$