Theorem oldsuc

Description: The value of the old set at a successor. (Contributed by Scott Fenton, 8-Aug-2024)

	Ref	Expression
Assertion	oldsuc	⊢ ( 𝐴 ∈ On → ( O ‘ suc 𝐴 ) = ( ( O ‘ 𝐴 ) ∪ ( N ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		madeoldsuc	⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = ( O ‘ suc 𝐴 ) )
2		madeun	⊢ ( M ‘ 𝐴 ) = ( ( O ‘ 𝐴 ) ∪ ( N ‘ 𝐴 ) )
3	1 2	eqtr3di	⊢ ( 𝐴 ∈ On → ( O ‘ suc 𝐴 ) = ( ( O ‘ 𝐴 ) ∪ ( N ‘ 𝐴 ) ) )