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 e. On -> ( har ` A ) = |^| { x e. ran card | A ~< x } )

Proof

Step	Hyp	Ref	Expression
1		onenon	|- ( A e. On -> A e. dom card )
2		harval3	|- ( A e. dom card -> ( har ` A ) = |^| { x e. ran card | A ~< x } )
3	1 2	syl	|- ( A e. On -> ( har ` A ) = |^| { x e. ran card | A ~< x } )