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	⊢ ( O ‘ 𝐴 ) ⊆ ( M ‘ 𝐴 )
23	22	a1i	⊢ ( 𝐴 ∈ On → ( O ‘ 𝐴 ) ⊆ ( M ‘ 𝐴 ) )
24		ssequn1	⊢ ( ( O ‘ 𝐴 ) ⊆ ( M ‘ 𝐴 ) ↔ ( ( O ‘ 𝐴 ) ∪ ( M ‘ 𝐴 ) ) = ( M ‘ 𝐴 ) )
25	23 24	sylib	⊢ ( 𝐴 ∈ On → ( ( O ‘ 𝐴 ) ∪ ( M ‘ 𝐴 ) ) = ( M ‘ 𝐴 ) )
26	8 21 25	3eqtrrd	⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = ∪ ( M “ suc 𝐴 ) )
27		suceloni	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )
28		oldval	⊢ ( suc 𝐴 ∈ On → ( O ‘ suc 𝐴 ) = ∪ ( M “ suc 𝐴 ) )
29	27 28	syl	⊢ ( 𝐴 ∈ On → ( O ‘ suc 𝐴 ) = ∪ ( M “ suc 𝐴 ) )
30	26 29	eqtr4d	⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = ( O ‘ suc 𝐴 ) )