Metamath Proof Explorer

Theorem oldlim

Description: The value of the old set at a limit ordinal. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion oldlim 
|- ( ( Lim A /\ A e. V ) -> ( _Old ` A ) = U. ( _Old " A ) )

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _M ` c ) ) ) -> c e. A )
2 limsuc 
 |-  ( Lim A -> ( c e. A <-> suc c e. A ) )
3 2 ad2antrr 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _M ` c ) ) ) -> ( c e. A <-> suc c e. A ) )
4 1 3 mpbid 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _M ` c ) ) ) -> suc c e. A )
5 simprr 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _M ` c ) ) ) -> x e. ( _M ` c ) )
6 limord 
 |-  ( Lim A -> Ord A )
7 elex 
 |-  ( A e. V -> A e. _V )
8 6 7 anim12i 
 |-  ( ( Lim A /\ A e. V ) -> ( Ord A /\ A e. _V ) )
9 elon2 
 |-  ( A e. On <-> ( Ord A /\ A e. _V ) )
10 8 9 sylibr 
 |-  ( ( Lim A /\ A e. V ) -> A e. On )
11 onelon 
 |-  ( ( A e. On /\ c e. A ) -> c e. On )
12 10 1 11 syl2an2r 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _M ` c ) ) ) -> c e. On )
13 madeoldsuc 
 |-  ( c e. On -> ( _M ` c ) = ( _Old ` suc c ) )
14 12 13 syl 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _M ` c ) ) ) -> ( _M ` c ) = ( _Old ` suc c ) )
15 5 14 eleqtrd 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _M ` c ) ) ) -> x e. ( _Old ` suc c ) )
16 fveq2 
 |-  ( b = suc c -> ( _Old ` b ) = ( _Old ` suc c ) )
17 16 eleq2d 
 |-  ( b = suc c -> ( x e. ( _Old ` b ) <-> x e. ( _Old ` suc c ) ) )
18 17 rspcev 
 |-  ( ( suc c e. A /\ x e. ( _Old ` suc c ) ) -> E. b e. A x e. ( _Old ` b ) )
19 4 15 18 syl2anc 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _M ` c ) ) ) -> E. b e. A x e. ( _Old ` b ) )
20 19 rexlimdvaa 
 |-  ( ( Lim A /\ A e. V ) -> ( E. c e. A x e. ( _M ` c ) -> E. b e. A x e. ( _Old ` b ) ) )
21 simprl 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( b e. A /\ x e. ( _Old ` b ) ) ) -> b e. A )
22 oldssmade 
 |-  ( _Old ` b ) C_ ( _M ` b )
23 simprr 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( b e. A /\ x e. ( _Old ` b ) ) ) -> x e. ( _Old ` b ) )
24 22 23 sselid 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( b e. A /\ x e. ( _Old ` b ) ) ) -> x e. ( _M ` b ) )
25 fveq2 
 |-  ( c = b -> ( _M ` c ) = ( _M ` b ) )
26 25 eleq2d 
 |-  ( c = b -> ( x e. ( _M ` c ) <-> x e. ( _M ` b ) ) )
27 26 rspcev 
 |-  ( ( b e. A /\ x e. ( _M ` b ) ) -> E. c e. A x e. ( _M ` c ) )
28 21 24 27 syl2anc 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( b e. A /\ x e. ( _Old ` b ) ) ) -> E. c e. A x e. ( _M ` c ) )
29 28 rexlimdvaa 
 |-  ( ( Lim A /\ A e. V ) -> ( E. b e. A x e. ( _Old ` b ) -> E. c e. A x e. ( _M ` c ) ) )
30 20 29 impbid 
 |-  ( ( Lim A /\ A e. V ) -> ( E. c e. A x e. ( _M ` c ) <-> E. b e. A x e. ( _Old ` b ) ) )
31 elold 
 |-  ( A e. On -> ( x e. ( _Old ` A ) <-> E. c e. A x e. ( _M ` c ) ) )
32 10 31 syl 
 |-  ( ( Lim A /\ A e. V ) -> ( x e. ( _Old ` A ) <-> E. c e. A x e. ( _M ` c ) ) )
33 eliun 
 |-  ( x e. U_ b e. A ( _Old ` b ) <-> E. b e. A x e. ( _Old ` b ) )
34 33 a1i 
 |-  ( ( Lim A /\ A e. V ) -> ( x e. U_ b e. A ( _Old ` b ) <-> E. b e. A x e. ( _Old ` b ) ) )
35 30 32 34 3bitr4d 
 |-  ( ( Lim A /\ A e. V ) -> ( x e. ( _Old ` A ) <-> x e. U_ b e. A ( _Old ` b ) ) )
36 35 eqrdv 
 |-  ( ( Lim A /\ A e. V ) -> ( _Old ` A ) = U_ b e. A ( _Old ` b ) )
37 oldf 
 |-  _Old : On --> ~P No
38 ffun 
 |-  ( _Old : On --> ~P No -> Fun _Old )
39 funiunfv 
 |-  ( Fun _Old -> U_ b e. A ( _Old ` b ) = U. ( _Old " A ) )
40 37 38 39 mp2b 
 |-  U_ b e. A ( _Old ` b ) = U. ( _Old " A )
41 36 40 eqtrdi 
 |-  ( ( Lim A /\ A e. V ) -> ( _Old ` A ) = U. ( _Old " A ) )