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 ` A ) = ( ( _Old ` A ) u. ( _N ` A ) )

Proof

Step	Hyp	Ref	Expression
1		newval	|- ( _N ` A ) = ( ( _M ` A ) \ ( _Old ` A ) )
2	1	uneq2i	|- ( ( _Old ` A ) u. ( _N ` A ) ) = ( ( _Old ` A ) u. ( ( _M ` A ) \ ( _Old ` A ) ) )
3		oldssmade	|- ( _Old ` A ) C_ ( _M ` A )
4		undif	|- ( ( _Old ` A ) C_ ( _M ` A ) <-> ( ( _Old ` A ) u. ( ( _M ` A ) \ ( _Old ` A ) ) ) = ( _M ` A ) )
5	3 4	mpbi	|- ( ( _Old ` A ) u. ( ( _M ` A ) \ ( _Old ` A ) ) ) = ( _M ` A )
6	2 5	eqtr2i	|- ( _M ` A ) = ( ( _Old ` A ) u. ( _N ` A ) )