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 expr 
 |-  ( ( ( Lim A /\ A e. V ) /\ c e. A ) -> ( x e. ( _M ` c ) -> E. b e. A x e. ( _Old ` b ) ) )
21 20 rexlimdva 
 |-  ( ( Lim A /\ A e. V ) -> ( E. c e. A x e. ( _M ` c ) -> E. b e. A x e. ( _Old ` b ) ) )
22 simprl 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( b e. A /\ x e. ( _Old ` b ) ) ) -> b e. A )
23 onelon 
 |-  ( ( A e. On /\ b e. A ) -> b e. On )
24 10 22 23 syl2an2r 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( b e. A /\ x e. ( _Old ` b ) ) ) -> b e. On )
25 oldssmade 
 |-  ( b e. On -> ( _Old ` b ) C_ ( _M ` b ) )
26 24 25 syl 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( b e. A /\ x e. ( _Old ` b ) ) ) -> ( _Old ` b ) C_ ( _M ` b ) )
27 simprr 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( b e. A /\ x e. ( _Old ` b ) ) ) -> x e. ( _Old ` b ) )
28 26 27 sseldd 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( b e. A /\ x e. ( _Old ` b ) ) ) -> x e. ( _M ` b ) )
29 fveq2 
 |-  ( c = b -> ( _M ` c ) = ( _M ` b ) )
30 29 eleq2d 
 |-  ( c = b -> ( x e. ( _M ` c ) <-> x e. ( _M ` b ) ) )
31 30 rspcev 
 |-  ( ( b e. A /\ x e. ( _M ` b ) ) -> E. c e. A x e. ( _M ` c ) )
32 22 28 31 syl2anc 
 |-  ( ( ( Lim A /\ A e. V ) /\ ( b e. A /\ x e. ( _Old ` b ) ) ) -> E. c e. A x e. ( _M ` c ) )
33 32 expr 
 |-  ( ( ( Lim A /\ A e. V ) /\ b e. A ) -> ( x e. ( _Old ` b ) -> E. c e. A x e. ( _M ` c ) ) )
34 33 rexlimdva 
 |-  ( ( Lim A /\ A e. V ) -> ( E. b e. A x e. ( _Old ` b ) -> E. c e. A x e. ( _M ` c ) ) )
35 21 34 impbid 
 |-  ( ( Lim A /\ A e. V ) -> ( E. c e. A x e. ( _M ` c ) <-> E. b e. A x e. ( _Old ` b ) ) )
36 elold 
 |-  ( A e. On -> ( x e. ( _Old ` A ) <-> E. c e. A x e. ( _M ` c ) ) )
37 10 36 syl 
 |-  ( ( Lim A /\ A e. V ) -> ( x e. ( _Old ` A ) <-> E. c e. A x e. ( _M ` c ) ) )
38 eliun 
 |-  ( x e. U_ b e. A ( _Old ` b ) <-> E. b e. A x e. ( _Old ` b ) )
39 38 a1i 
 |-  ( ( Lim A /\ A e. V ) -> ( x e. U_ b e. A ( _Old ` b ) <-> E. b e. A x e. ( _Old ` b ) ) )
40 35 37 39 3bitr4d 
 |-  ( ( Lim A /\ A e. V ) -> ( x e. ( _Old ` A ) <-> x e. U_ b e. A ( _Old ` b ) ) )
41 40 eqrdv 
 |-  ( ( Lim A /\ A e. V ) -> ( _Old ` A ) = U_ b e. A ( _Old ` b ) )
42 oldf 
 |-  _Old : On --> ~P No
43 ffun 
 |-  ( _Old : On --> ~P No -> Fun _Old )
44 funiunfv 
 |-  ( Fun _Old -> U_ b e. A ( _Old ` b ) = U. ( _Old " A ) )
45 42 43 44 mp2b 
 |-  U_ b e. A ( _Old ` b ) = U. ( _Old " A )
46 41 45 eqtrdi 
 |-  ( ( Lim A /\ A e. V ) -> ( _Old ` A ) = U. ( _Old " A ) )