Theorem madeoldsuc

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

	Ref	Expression
Assertion	madeoldsuc	⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = ( O ‘ suc 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
2	1	imaeq2i	⊢ ( M “ suc 𝐴 ) = ( M “ ( 𝐴 ∪ { 𝐴 } ) )
3		imaundi	⊢ ( M “ ( 𝐴 ∪ { 𝐴 } ) ) = ( ( M “ 𝐴 ) ∪ ( M “ { 𝐴 } ) )
4	2 3	eqtri	⊢ ( M “ suc 𝐴 ) = ( ( M “ 𝐴 ) ∪ ( M “ { 𝐴 } ) )
5	4	unieqi	⊢ ∪ ( M “ suc 𝐴 ) = ∪ ( ( M “ 𝐴 ) ∪ ( M “ { 𝐴 } ) )
6		uniun	⊢ ∪ ( ( M “ 𝐴 ) ∪ ( M “ { 𝐴 } ) ) = ( ∪ ( M “ 𝐴 ) ∪ ∪ ( M “ { 𝐴 } ) )
7	5 6	eqtri	⊢ ∪ ( M “ suc 𝐴 ) = ( ∪ ( M “ 𝐴 ) ∪ ∪ ( M “ { 𝐴 } ) )
8	7	a1i	⊢ ( 𝐴 ∈ On → ∪ ( M “ suc 𝐴 ) = ( ∪ ( M “ 𝐴 ) ∪ ∪ ( M “ { 𝐴 } ) ) )
9		oldval	⊢ ( 𝐴 ∈ On → ( O ‘ 𝐴 ) = ∪ ( M “ 𝐴 ) )
10	9	eqcomd	⊢ ( 𝐴 ∈ On → ∪ ( M “ 𝐴 ) = ( O ‘ 𝐴 ) )
11		madef	⊢ M : On ⟶ 𝒫 No
12		ffn	⊢ ( M : On ⟶ 𝒫 No → M Fn On )
13	11 12	ax-mp	⊢ M Fn On
14		fnsnfv	⊢ ( ( M Fn On ∧ 𝐴 ∈ On ) → { ( M ‘ 𝐴 ) } = ( M “ { 𝐴 } ) )
15	14	eqcomd	⊢ ( ( M Fn On ∧ 𝐴 ∈ On ) → ( M “ { 𝐴 } ) = { ( M ‘ 𝐴 ) } )
16	13 15	mpan	⊢ ( 𝐴 ∈ On → ( M “ { 𝐴 } ) = { ( M ‘ 𝐴 ) } )
17	16	unieqd	⊢ ( 𝐴 ∈ On → ∪ ( M “ { 𝐴 } ) = ∪ { ( M ‘ 𝐴 ) } )
18		fvex	⊢ ( M ‘ 𝐴 ) ∈ V
19	18	unisn	⊢ ∪ { ( M ‘ 𝐴 ) } = ( M ‘ 𝐴 )
20	17 19	eqtrdi	⊢ ( 𝐴 ∈ On → ∪ ( M “ { 𝐴 } ) = ( M ‘ 𝐴 ) )
21	10 20	uneq12d	⊢ ( 𝐴 ∈ On → ( ∪ ( M “ 𝐴 ) ∪ ∪ ( M “ { 𝐴 } ) ) = ( ( O ‘ 𝐴 ) ∪ ( M ‘ 𝐴 ) ) )
22		oldssmade	⊢ ( 𝐴 ∈ On → ( O ‘ 𝐴 ) ⊆ ( M ‘ 𝐴 ) )
23		ssequn1	⊢ ( ( O ‘ 𝐴 ) ⊆ ( M ‘ 𝐴 ) ↔ ( ( O ‘ 𝐴 ) ∪ ( M ‘ 𝐴 ) ) = ( M ‘ 𝐴 ) )
24	22 23	sylib	⊢ ( 𝐴 ∈ On → ( ( O ‘ 𝐴 ) ∪ ( M ‘ 𝐴 ) ) = ( M ‘ 𝐴 ) )
25	8 21 24	3eqtrrd	⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = ∪ ( M “ suc 𝐴 ) )
26		suceloni	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )
27		oldval	⊢ ( suc 𝐴 ∈ On → ( O ‘ suc 𝐴 ) = ∪ ( M “ suc 𝐴 ) )
28	26 27	syl	⊢ ( 𝐴 ∈ On → ( O ‘ suc 𝐴 ) = ∪ ( M “ suc 𝐴 ) )
29	25 28	eqtr4d	⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = ( O ‘ suc 𝐴 ) )