Metamath Proof Explorer

Theorem oldfib

Description: The old set of an ordinal is finite iff the ordinal is finite. (Contributed by Scott Fenton, 19-Feb-2026)

Ref Expression
Assertion oldfib 
|- ( A e. On -> ( A e. _om <-> ( _Old ` A ) e. Fin ) )

Proof

Step Hyp Ref Expression
1 oldfi 
 |-  ( A e. _om -> ( _Old ` A ) e. Fin )
2 fveq2 
 |-  ( x = y -> ( _Old ` x ) = ( _Old ` y ) )
3 2 eleq1d 
 |-  ( x = y -> ( ( _Old ` x ) e. Fin <-> ( _Old ` y ) e. Fin ) )
4 eleq1 
 |-  ( x = y -> ( x e. _om <-> y e. _om ) )
5 3 4 imbi12d 
 |-  ( x = y -> ( ( ( _Old ` x ) e. Fin -> x e. _om ) <-> ( ( _Old ` y ) e. Fin -> y e. _om ) ) )
6 fveq2 
 |-  ( x = A -> ( _Old ` x ) = ( _Old ` A ) )
7 6 eleq1d 
 |-  ( x = A -> ( ( _Old ` x ) e. Fin <-> ( _Old ` A ) e. Fin ) )
8 eleq1 
 |-  ( x = A -> ( x e. _om <-> A e. _om ) )
9 7 8 imbi12d 
 |-  ( x = A -> ( ( ( _Old ` x ) e. Fin -> x e. _om ) <-> ( ( _Old ` A ) e. Fin -> A e. _om ) ) )
10 oldval 
 |-  ( x e. On -> ( _Old ` x ) = U. ( _Made " x ) )
11 10 eleq1d 
 |-  ( x e. On -> ( ( _Old ` x ) e. Fin <-> U. ( _Made " x ) e. Fin ) )
12 11 biimpa 
 |-  ( ( x e. On /\ ( _Old ` x ) e. Fin ) -> U. ( _Made " x ) e. Fin )
13 unifi3 
 |-  ( U. ( _Made " x ) e. Fin -> ( _Made " x ) C_ Fin )
14 12 13 syl 
 |-  ( ( x e. On /\ ( _Old ` x ) e. Fin ) -> ( _Made " x ) C_ Fin )
15 madef 
 |-  _Made : On --> ~P No
16 ffun 
 |-  ( _Made : On --> ~P No -> Fun _Made )
17 15 16 ax-mp 
 |-  Fun _Made
18 onss 
 |-  ( x e. On -> x C_ On )
19 15 fdmi 
 |-  dom _Made = On
20 18 19 sseqtrrdi 
 |-  ( x e. On -> x C_ dom _Made )
21 funimass4 
 |-  ( ( Fun _Made /\ x C_ dom _Made ) -> ( ( _Made " x ) C_ Fin <-> A. y e. x ( _Made ` y ) e. Fin ) )
22 17 20 21 sylancr 
 |-  ( x e. On -> ( ( _Made " x ) C_ Fin <-> A. y e. x ( _Made ` y ) e. Fin ) )
23 22 adantr 
 |-  ( ( x e. On /\ ( _Old ` x ) e. Fin ) -> ( ( _Made " x ) C_ Fin <-> A. y e. x ( _Made ` y ) e. Fin ) )
24 14 23 mpbid 
 |-  ( ( x e. On /\ ( _Old ` x ) e. Fin ) -> A. y e. x ( _Made ` y ) e. Fin )
25 oldssmade 
 |-  ( _Old ` y ) C_ ( _Made ` y )
26 ssfi 
 |-  ( ( ( _Made ` y ) e. Fin /\ ( _Old ` y ) C_ ( _Made ` y ) ) -> ( _Old ` y ) e. Fin )
27 25 26 mpan2 
 |-  ( ( _Made ` y ) e. Fin -> ( _Old ` y ) e. Fin )
28 27 ralimi 
 |-  ( A. y e. x ( _Made ` y ) e. Fin -> A. y e. x ( _Old ` y ) e. Fin )
29 24 28 syl 
 |-  ( ( x e. On /\ ( _Old ` x ) e. Fin ) -> A. y e. x ( _Old ` y ) e. Fin )
30 29 3adant2 
 |-  ( ( x e. On /\ A. y e. x ( ( _Old ` y ) e. Fin -> y e. _om ) /\ ( _Old ` x ) e. Fin ) -> A. y e. x ( _Old ` y ) e. Fin )
31 r19.26 
 |-  ( A. y e. x ( ( ( _Old ` y ) e. Fin -> y e. _om ) /\ ( _Old ` y ) e. Fin ) <-> ( A. y e. x ( ( _Old ` y ) e. Fin -> y e. _om ) /\ A. y e. x ( _Old ` y ) e. Fin ) )
32 pm2.27 
 |-  ( ( _Old ` y ) e. Fin -> ( ( ( _Old ` y ) e. Fin -> y e. _om ) -> y e. _om ) )
33 32 impcom 
 |-  ( ( ( ( _Old ` y ) e. Fin -> y e. _om ) /\ ( _Old ` y ) e. Fin ) -> y e. _om )
34 33 ralimi 
 |-  ( A. y e. x ( ( ( _Old ` y ) e. Fin -> y e. _om ) /\ ( _Old ` y ) e. Fin ) -> A. y e. x y e. _om )
35 dfss3 
 |-  ( x C_ _om <-> A. y e. x y e. _om )
36 34 35 sylibr 
 |-  ( A. y e. x ( ( ( _Old ` y ) e. Fin -> y e. _om ) /\ ( _Old ` y ) e. Fin ) -> x C_ _om )
37 31 36 sylbir 
 |-  ( ( A. y e. x ( ( _Old ` y ) e. Fin -> y e. _om ) /\ A. y e. x ( _Old ` y ) e. Fin ) -> x C_ _om )
38 eloni 
 |-  ( x e. On -> Ord x )
39 ordom 
 |-  Ord _om
40 ordsseleq 
 |-  ( ( Ord x /\ Ord _om ) -> ( x C_ _om <-> ( x e. _om \/ x = _om ) ) )
41 39 40 mpan2 
 |-  ( Ord x -> ( x C_ _om <-> ( x e. _om \/ x = _om ) ) )
42 38 41 syl 
 |-  ( x e. On -> ( x C_ _om <-> ( x e. _om \/ x = _om ) ) )
43 42 adantr 
 |-  ( ( x e. On /\ ( _Old ` x ) e. Fin ) -> ( x C_ _om <-> ( x e. _om \/ x = _om ) ) )
44 fveq2 
 |-  ( x = _om -> ( _Old ` x ) = ( _Old ` _om ) )
45 eqvisset 
 |-  ( x = _om -> _om e. _V )
46 bdayfun 
 |-  Fun bday
47 n0sexg 
 |-  ( _om e. _V -> NN0_s e. _V )
48 resfunexg 
 |-  ( ( Fun bday /\ NN0_s e. _V ) -> ( bday |` NN0_s ) e. _V )
49 46 47 48 sylancr 
 |-  ( _om e. _V -> ( bday |` NN0_s ) e. _V )
50 cnvexg 
 |-  ( ( bday |` NN0_s ) e. _V -> `' ( bday |` NN0_s ) e. _V )
51 49 50 syl 
 |-  ( _om e. _V -> `' ( bday |` NN0_s ) e. _V )
52 bdayn0sf1o 
 |-  ( bday |` NN0_s ) : NN0_s -1-1-onto-> _om
53 52 a1i 
 |-  ( _om e. _V -> ( bday |` NN0_s ) : NN0_s -1-1-onto-> _om )
54 f1ocnv 
 |-  ( ( bday |` NN0_s ) : NN0_s -1-1-onto-> _om -> `' ( bday |` NN0_s ) : _om -1-1-onto-> NN0_s )
55 f1of1 
 |-  ( `' ( bday |` NN0_s ) : _om -1-1-onto-> NN0_s -> `' ( bday |` NN0_s ) : _om -1-1-> NN0_s )
56 53 54 55 3syl 
 |-  ( _om e. _V -> `' ( bday |` NN0_s ) : _om -1-1-> NN0_s )
57 n0ssoldg 
 |-  ( _om e. _V -> NN0_s C_ ( _Old ` _om ) )
58 f1ss 
 |-  ( ( `' ( bday |` NN0_s ) : _om -1-1-> NN0_s /\ NN0_s C_ ( _Old ` _om ) ) -> `' ( bday |` NN0_s ) : _om -1-1-> ( _Old ` _om ) )
59 56 57 58 syl2anc 
 |-  ( _om e. _V -> `' ( bday |` NN0_s ) : _om -1-1-> ( _Old ` _om ) )
60 f1eq1 
 |-  ( f = `' ( bday |` NN0_s ) -> ( f : _om -1-1-> ( _Old ` _om ) <-> `' ( bday |` NN0_s ) : _om -1-1-> ( _Old ` _om ) ) )
61 51 59 60 spcedv 
 |-  ( _om e. _V -> E. f f : _om -1-1-> ( _Old ` _om ) )
62 fvex 
 |-  ( _Old ` _om ) e. _V
63 62 brdom 
 |-  ( _om ~<_ ( _Old ` _om ) <-> E. f f : _om -1-1-> ( _Old ` _om ) )
64 61 63 sylibr 
 |-  ( _om e. _V -> _om ~<_ ( _Old ` _om ) )
65 infinfg 
 |-  ( ( _om e. _V /\ ( _Old ` _om ) e. _V ) -> ( -. ( _Old ` _om ) e. Fin <-> _om ~<_ ( _Old ` _om ) ) )
66 62 65 mpan2 
 |-  ( _om e. _V -> ( -. ( _Old ` _om ) e. Fin <-> _om ~<_ ( _Old ` _om ) ) )
67 64 66 mpbird 
 |-  ( _om e. _V -> -. ( _Old ` _om ) e. Fin )
68 45 67 syl 
 |-  ( x = _om -> -. ( _Old ` _om ) e. Fin )
69 44 68 eqneltrd 
 |-  ( x = _om -> -. ( _Old ` x ) e. Fin )
70 69 con2i 
 |-  ( ( _Old ` x ) e. Fin -> -. x = _om )
71 70 adantl 
 |-  ( ( x e. On /\ ( _Old ` x ) e. Fin ) -> -. x = _om )
72 orel2 
 |-  ( -. x = _om -> ( ( x e. _om \/ x = _om ) -> x e. _om ) )
73 71 72 syl 
 |-  ( ( x e. On /\ ( _Old ` x ) e. Fin ) -> ( ( x e. _om \/ x = _om ) -> x e. _om ) )
74 43 73 sylbid 
 |-  ( ( x e. On /\ ( _Old ` x ) e. Fin ) -> ( x C_ _om -> x e. _om ) )
75 37 74 syl5 
 |-  ( ( x e. On /\ ( _Old ` x ) e. Fin ) -> ( ( A. y e. x ( ( _Old ` y ) e. Fin -> y e. _om ) /\ A. y e. x ( _Old ` y ) e. Fin ) -> x e. _om ) )
76 75 expd 
 |-  ( ( x e. On /\ ( _Old ` x ) e. Fin ) -> ( A. y e. x ( ( _Old ` y ) e. Fin -> y e. _om ) -> ( A. y e. x ( _Old ` y ) e. Fin -> x e. _om ) ) )
77 76 3impia 
 |-  ( ( x e. On /\ ( _Old ` x ) e. Fin /\ A. y e. x ( ( _Old ` y ) e. Fin -> y e. _om ) ) -> ( A. y e. x ( _Old ` y ) e. Fin -> x e. _om ) )
78 77 3com23 
 |-  ( ( x e. On /\ A. y e. x ( ( _Old ` y ) e. Fin -> y e. _om ) /\ ( _Old ` x ) e. Fin ) -> ( A. y e. x ( _Old ` y ) e. Fin -> x e. _om ) )
79 30 78 mpd 
 |-  ( ( x e. On /\ A. y e. x ( ( _Old ` y ) e. Fin -> y e. _om ) /\ ( _Old ` x ) e. Fin ) -> x e. _om )
80 79 3exp 
 |-  ( x e. On -> ( A. y e. x ( ( _Old ` y ) e. Fin -> y e. _om ) -> ( ( _Old ` x ) e. Fin -> x e. _om ) ) )
81 5 9 80 tfis3 
 |-  ( A e. On -> ( ( _Old ` A ) e. Fin -> A e. _om ) )
82 1 81 impbid2 
 |-  ( A e. On -> ( A e. _om <-> ( _Old ` A ) e. Fin ) )