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 e. On -> ( _M ` A ) = ( _Old ` suc A ) )

Proof

Step	Hyp	Ref	Expression
1		df-suc	|- suc A = ( A u. { A } )
2	1	imaeq2i	|- ( _M " suc A ) = ( _M " ( A u. { A } ) )
3		imaundi	|- ( _M " ( A u. { A } ) ) = ( ( _M " A ) u. ( _M " { A } ) )
4	2 3	eqtri	|- ( _M " suc A ) = ( ( _M " A ) u. ( _M " { A } ) )
5	4	unieqi	|- U. ( _M " suc A ) = U. ( ( _M " A ) u. ( _M " { A } ) )
6		uniun	|- U. ( ( _M " A ) u. ( _M " { A } ) ) = ( U. ( _M " A ) u. U. ( _M " { A } ) )
7	5 6	eqtri	|- U. ( _M " suc A ) = ( U. ( _M " A ) u. U. ( _M " { A } ) )
8	7	a1i	|- ( A e. On -> U. ( _M " suc A ) = ( U. ( _M " A ) u. U. ( _M " { A } ) ) )
9		oldval	|- ( A e. On -> ( _Old ` A ) = U. ( _M " A ) )
10	9	eqcomd	|- ( A e. On -> U. ( _M " A ) = ( _Old ` A ) )
11		madef	|- _M : On --> ~P No
12		ffn	|- ( _M : On --> ~P No -> _M Fn On )
13	11 12	ax-mp	|- _M Fn On
14		fnsnfv	|- ( ( _M Fn On /\ A e. On ) -> { ( _M ` A ) } = ( _M " { A } ) )
15	14	eqcomd	|- ( ( _M Fn On /\ A e. On ) -> ( _M " { A } ) = { ( _M ` A ) } )
16	13 15	mpan	|- ( A e. On -> ( _M " { A } ) = { ( _M ` A ) } )
17	16	unieqd	|- ( A e. On -> U. ( _M " { A } ) = U. { ( _M ` A ) } )
18		fvex	|- ( _M ` A ) e. _V
19	18	unisn	|- U. { ( _M ` A ) } = ( _M ` A )
20	17 19	eqtrdi	|- ( A e. On -> U. ( _M " { A } ) = ( _M ` A ) )
21	10 20	uneq12d	|- ( A e. On -> ( U. ( _M " A ) u. U. ( _M " { A } ) ) = ( ( _Old ` A ) u. ( _M ` A ) ) )
22		oldssmade	|- ( _Old ` A ) C_ ( _M ` A )
23	22	a1i	|- ( A e. On -> ( _Old ` A ) C_ ( _M ` A ) )
24		ssequn1	|- ( ( _Old ` A ) C_ ( _M ` A ) <-> ( ( _Old ` A ) u. ( _M ` A ) ) = ( _M ` A ) )
25	23 24	sylib	|- ( A e. On -> ( ( _Old ` A ) u. ( _M ` A ) ) = ( _M ` A ) )
26	8 21 25	3eqtrrd	|- ( A e. On -> ( _M ` A ) = U. ( _M " suc A ) )
27		suceloni	|- ( A e. On -> suc A e. On )
28		oldval	|- ( suc A e. On -> ( _Old ` suc A ) = U. ( _M " suc A ) )
29	27 28	syl	|- ( A e. On -> ( _Old ` suc A ) = U. ( _M " suc A ) )
30	26 29	eqtr4d	|- ( A e. On -> ( _M ` A ) = ( _Old ` suc A ) )