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	⊢ ( 𝐴 ∈ On → ( har ‘ 𝐴 ) = ∩ { 𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		onenon	⊢ ( 𝐴 ∈ On → 𝐴 ∈ dom card )
2		harval3	⊢ ( 𝐴 ∈ dom card → ( har ‘ 𝐴 ) = ∩ { 𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥 } )
3	1 2	syl	⊢ ( 𝐴 ∈ On → ( har ‘ 𝐴 ) = ∩ { 𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥 } )