Theorem oldsuc

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

	Ref	Expression
Assertion	oldsuc	$$⊢A\in \mathrm{On}\to \mathrm{Old}\left(\mathrm{suc}A\right)=\mathrm{Old}\left(A\right)\cup N\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		madeoldsuc	$$⊢A\in \mathrm{On}\to M\left(A\right)=\mathrm{Old}\left(\mathrm{suc}A\right)$$
2		madeun	$$⊢M\left(A\right)=\mathrm{Old}\left(A\right)\cup N\left(A\right)$$
3	1 2	eqtr3di	$$⊢A\in \mathrm{On}\to \mathrm{Old}\left(\mathrm{suc}A\right)=\mathrm{Old}\left(A\right)\cup N\left(A\right)$$