Theorem harval3on

Description: For any ordinal number A let ( harA ) denote the least cardinal that is greater than A ; (Contributed by RP, 4-Nov-2023)

	Ref	Expression
Assertion	harval3on	$$⊢A\in \mathrm{On}\to \mathrm{har}\left(A\right)=\bigcap \left\{x\in \mathrm{ran}\mathrm{card}|A\prec x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		onenon	$$⊢A\in \mathrm{On}\to A\in \mathrm{dom}\mathrm{card}$$
2		harval3	$$⊢A\in \mathrm{dom}\mathrm{card}\to \mathrm{har}\left(A\right)=\bigcap \left\{x\in \mathrm{ran}\mathrm{card}|A\prec x\right\}$$
3	1 2	syl	$$⊢A\in \mathrm{On}\to \mathrm{har}\left(A\right)=\bigcap \left\{x\in \mathrm{ran}\mathrm{card}|A\prec x\right\}$$