Theorem madeun

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

	Ref	Expression
Assertion	madeun	⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = ( ( O ‘ 𝐴 ) ∪ ( N ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		newval	⊢ ( 𝐴 ∈ On → ( N ‘ 𝐴 ) = ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) )
2	1	uneq2d	⊢ ( 𝐴 ∈ On → ( ( O ‘ 𝐴 ) ∪ ( N ‘ 𝐴 ) ) = ( ( O ‘ 𝐴 ) ∪ ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) ) )
3		oldssmade	⊢ ( 𝐴 ∈ On → ( O ‘ 𝐴 ) ⊆ ( M ‘ 𝐴 ) )
4		undif	⊢ ( ( O ‘ 𝐴 ) ⊆ ( M ‘ 𝐴 ) ↔ ( ( O ‘ 𝐴 ) ∪ ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) ) = ( M ‘ 𝐴 ) )
5	3 4	sylib	⊢ ( 𝐴 ∈ On → ( ( O ‘ 𝐴 ) ∪ ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) ) = ( M ‘ 𝐴 ) )
6	2 5	eqtr2d	⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = ( ( O ‘ 𝐴 ) ∪ ( N ‘ 𝐴 ) ) )