Theorem madeun

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

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

Proof

Step	Hyp	Ref	Expression
1		newval	⊢ ( N ‘ 𝐴 ) = ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) )
2	1	uneq2i	⊢ ( ( O ‘ 𝐴 ) ∪ ( N ‘ 𝐴 ) ) = ( ( O ‘ 𝐴 ) ∪ ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) )
3		oldssmade	⊢ ( O ‘ 𝐴 ) ⊆ ( M ‘ 𝐴 )
4		undif	⊢ ( ( O ‘ 𝐴 ) ⊆ ( M ‘ 𝐴 ) ↔ ( ( O ‘ 𝐴 ) ∪ ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) ) = ( M ‘ 𝐴 ) )
5	3 4	mpbi	⊢ ( ( O ‘ 𝐴 ) ∪ ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) ) = ( M ‘ 𝐴 )
6	2 5	eqtr2i	⊢ ( M ‘ 𝐴 ) = ( ( O ‘ 𝐴 ) ∪ ( N ‘ 𝐴 ) )