Metamath Proof Explorer

Theorem madeoldsuc

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

Ref Expression
Assertion madeoldsuc 
|- ( A e. On -> ( _M ` A ) = ( _Old ` suc A ) )

Proof

Step Hyp Ref Expression
1 df-suc 
 |-  suc A = ( A u. { A } )
2 1 imaeq2i 
 |-  ( _M " suc A ) = ( _M " ( A u. { A } ) )
3 imaundi 
 |-  ( _M " ( A u. { A } ) ) = ( ( _M " A ) u. ( _M " { A } ) )
4 2 3 eqtri 
 |-  ( _M " suc A ) = ( ( _M " A ) u. ( _M " { A } ) )
5 4 unieqi 
 |-  U. ( _M " suc A ) = U. ( ( _M " A ) u. ( _M " { A } ) )
6 uniun 
 |-  U. ( ( _M " A ) u. ( _M " { A } ) ) = ( U. ( _M " A ) u. U. ( _M " { A } ) )
7 5 6 eqtri 
 |-  U. ( _M " suc A ) = ( U. ( _M " A ) u. U. ( _M " { A } ) )
8 7 a1i 
 |-  ( A e. On -> U. ( _M " suc A ) = ( U. ( _M " A ) u. U. ( _M " { A } ) ) )
9 oldval 
 |-  ( A e. On -> ( _Old ` A ) = U. ( _M " A ) )
10 9 eqcomd 
 |-  ( A e. On -> U. ( _M " A ) = ( _Old ` A ) )
11 madef 
 |-  _M : On --> ~P No
12 ffn 
 |-  ( _M : On --> ~P No -> _M Fn On )
13 11 12 ax-mp 
 |-  _M Fn On
14 fnsnfv 
 |-  ( ( _M Fn On /\ A e. On ) -> { ( _M ` A ) } = ( _M " { A } ) )
15 14 eqcomd 
 |-  ( ( _M Fn On /\ A e. On ) -> ( _M " { A } ) = { ( _M ` A ) } )
16 13 15 mpan 
 |-  ( A e. On -> ( _M " { A } ) = { ( _M ` A ) } )
17 16 unieqd 
 |-  ( A e. On -> U. ( _M " { A } ) = U. { ( _M ` A ) } )
18 fvex 
 |-  ( _M ` A ) e. _V
19 18 unisn 
 |-  U. { ( _M ` A ) } = ( _M ` A )
20 17 19 eqtrdi 
 |-  ( A e. On -> U. ( _M " { A } ) = ( _M ` A ) )
21 10 20 uneq12d 
 |-  ( A e. On -> ( U. ( _M " A ) u. U. ( _M " { A } ) ) = ( ( _Old ` A ) u. ( _M ` A ) ) )
22 oldssmade 
 |-  ( A e. On -> ( _Old ` A ) C_ ( _M ` A ) )
23 ssequn1 
 |-  ( ( _Old ` A ) C_ ( _M ` A ) <-> ( ( _Old ` A ) u. ( _M ` A ) ) = ( _M ` A ) )
24 22 23 sylib 
 |-  ( A e. On -> ( ( _Old ` A ) u. ( _M ` A ) ) = ( _M ` A ) )
25 8 21 24 3eqtrrd 
 |-  ( A e. On -> ( _M ` A ) = U. ( _M " suc A ) )
26 suceloni 
 |-  ( A e. On -> suc A e. On )
27 oldval 
 |-  ( suc A e. On -> ( _Old ` suc A ) = U. ( _M " suc A ) )
28 26 27 syl 
 |-  ( A e. On -> ( _Old ` suc A ) = U. ( _M " suc A ) )
29 25 28 eqtr4d 
 |-  ( A e. On -> ( _M ` A ) = ( _Old ` suc A ) )