Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 newval 
 |-  ( A e. On -> ( _N ` A ) = ( ( _M ` A ) \ ( _Old ` A ) ) )
2 1 uneq2d 
 |-  ( A e. On -> ( ( _Old ` A ) u. ( _N ` A ) ) = ( ( _Old ` A ) u. ( ( _M ` A ) \ ( _Old ` A ) ) ) )
3 oldssmade 
 |-  ( A e. On -> ( _Old ` A ) C_ ( _M ` A ) )
4 undif 
 |-  ( ( _Old ` A ) C_ ( _M ` A ) <-> ( ( _Old ` A ) u. ( ( _M ` A ) \ ( _Old ` A ) ) ) = ( _M ` A ) )
5 3 4 sylib 
 |-  ( A e. On -> ( ( _Old ` A ) u. ( ( _M ` A ) \ ( _Old ` A ) ) ) = ( _M ` A ) )
6 2 5 eqtr2d 
 |-  ( A e. On -> ( _M ` A ) = ( ( _Old ` A ) u. ( _N ` A ) ) )