Theorem madeoldsuc

Description: The made set is the old set of its successor. (Contributed by Scott Fenton, 8-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
2	1	imaeq2i	$$⊢M\left[\mathrm{suc}A\right]=M\left[A\cup \left\{A\right\}\right]$$
3		imaundi	$$⊢M\left[A\cup \left\{A\right\}\right]=M\left[A\right]\cup M\left[\left\{A\right\}\right]$$
4	2 3	eqtri	$$⊢M\left[\mathrm{suc}A\right]=M\left[A\right]\cup M\left[\left\{A\right\}\right]$$
5	4	unieqi	$$⊢\bigcup M\left[\mathrm{suc}A\right]=\bigcup \left(M\left[A\right]\cup M\left[\left\{A\right\}\right]\right)$$
6		uniun	$$⊢\bigcup \left(M\left[A\right]\cup M\left[\left\{A\right\}\right]\right)=\bigcup M\left[A\right]\cup \bigcup M\left[\left\{A\right\}\right]$$
7	5 6	eqtri	$$⊢\bigcup M\left[\mathrm{suc}A\right]=\bigcup M\left[A\right]\cup \bigcup M\left[\left\{A\right\}\right]$$
8	7	a1i	$$⊢A\in \mathrm{On}\to \bigcup M\left[\mathrm{suc}A\right]=\bigcup M\left[A\right]\cup \bigcup M\left[\left\{A\right\}\right]$$
9		oldval	$$⊢A\in \mathrm{On}\to \mathrm{Old}\left(A\right)=\bigcup M\left[A\right]$$
10	9	eqcomd	$$⊢A\in \mathrm{On}\to \bigcup M\left[A\right]=\mathrm{Old}\left(A\right)$$
11		madef	$$⊢M:\mathrm{On}⟶𝒫\mathrm{No}$$
12		ffn	$$⊢M:\mathrm{On}⟶𝒫\mathrm{No}\to MFn\mathrm{On}$$
13	11 12	ax-mp	$$⊢MFn\mathrm{On}$$
14		fnsnfv	$$⊢\left(MFn\mathrm{On}\wedge A\in \mathrm{On}\right)\to \left\{M\left(A\right)\right\}=M\left[\left\{A\right\}\right]$$
15	14	eqcomd	$$⊢\left(MFn\mathrm{On}\wedge A\in \mathrm{On}\right)\to M\left[\left\{A\right\}\right]=\left\{M\left(A\right)\right\}$$
16	13 15	mpan	$$⊢A\in \mathrm{On}\to M\left[\left\{A\right\}\right]=\left\{M\left(A\right)\right\}$$
17	16	unieqd	$$⊢A\in \mathrm{On}\to \bigcup M\left[\left\{A\right\}\right]=\bigcup \left\{M\left(A\right)\right\}$$
18		fvex	$$⊢M\left(A\right)\in \mathrm{V}$$
19	18	unisn	$$⊢\bigcup \left\{M\left(A\right)\right\}=M\left(A\right)$$
20	17 19	eqtrdi	$$⊢A\in \mathrm{On}\to \bigcup M\left[\left\{A\right\}\right]=M\left(A\right)$$
21	10 20	uneq12d	$$⊢A\in \mathrm{On}\to \bigcup M\left[A\right]\cup \bigcup M\left[\left\{A\right\}\right]=\mathrm{Old}\left(A\right)\cup M\left(A\right)$$
22		oldssmade	$$⊢\mathrm{Old}\left(A\right)\subseteq M\left(A\right)$$
23	22	a1i	$$⊢A\in \mathrm{On}\to \mathrm{Old}\left(A\right)\subseteq M\left(A\right)$$
24		ssequn1	$$⊢\mathrm{Old}\left(A\right)\subseteq M\left(A\right)\leftrightarrow \mathrm{Old}\left(A\right)\cup M\left(A\right)=M\left(A\right)$$
25	23 24	sylib	$$⊢A\in \mathrm{On}\to \mathrm{Old}\left(A\right)\cup M\left(A\right)=M\left(A\right)$$
26	8 21 25	3eqtrrd	$$⊢A\in \mathrm{On}\to M\left(A\right)=\bigcup M\left[\mathrm{suc}A\right]$$
27		suceloni	$$⊢A\in \mathrm{On}\to \mathrm{suc}A\in \mathrm{On}$$
28		oldval	$$⊢\mathrm{suc}A\in \mathrm{On}\to \mathrm{Old}\left(\mathrm{suc}A\right)=\bigcup M\left[\mathrm{suc}A\right]$$
29	27 28	syl	$$⊢A\in \mathrm{On}\to \mathrm{Old}\left(\mathrm{suc}A\right)=\bigcup M\left[\mathrm{suc}A\right]$$
30	26 29	eqtr4d	$$⊢A\in \mathrm{On}\to M\left(A\right)=\mathrm{Old}\left(\mathrm{suc}A\right)$$