Metamath Proof Explorer

Theorem madefi

Description: The made set of an ordinal natural is finite. (Contributed by Scott Fenton, 20-Aug-2025)

Ref Expression
Assertion madefi 
|- ( A e. _om -> ( _Made ` A ) e. Fin )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = y -> ( _Made ` x ) = ( _Made ` y ) )
2 1 eleq1d 
 |-  ( x = y -> ( ( _Made ` x ) e. Fin <-> ( _Made ` y ) e. Fin ) )
3 fveq2 
 |-  ( x = A -> ( _Made ` x ) = ( _Made ` A ) )
4 3 eleq1d 
 |-  ( x = A -> ( ( _Made ` x ) e. Fin <-> ( _Made ` A ) e. Fin ) )
5 nnon 
 |-  ( x e. _om -> x e. On )
6 madeval 
 |-  ( x e. On -> ( _Made ` x ) = ( |s " ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) ) )
7 5 6 syl 
 |-  ( x e. _om -> ( _Made ` x ) = ( |s " ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) ) )
8 7 adantr 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> ( _Made ` x ) = ( |s " ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) ) )
9 madef 
 |-  _Made : On --> ~P No
10 ffun 
 |-  ( _Made : On --> ~P No -> Fun _Made )
11 9 10 ax-mp 
 |-  Fun _Made
12 nnfi 
 |-  ( x e. _om -> x e. Fin )
13 imafi 
 |-  ( ( Fun _Made /\ x e. Fin ) -> ( _Made " x ) e. Fin )
14 11 12 13 sylancr 
 |-  ( x e. _om -> ( _Made " x ) e. Fin )
15 14 adantr 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> ( _Made " x ) e. Fin )
16 onss 
 |-  ( x e. On -> x C_ On )
17 5 16 syl 
 |-  ( x e. _om -> x C_ On )
18 9 fdmi 
 |-  dom _Made = On
19 17 18 sseqtrrdi 
 |-  ( x e. _om -> x C_ dom _Made )
20 funimass4 
 |-  ( ( Fun _Made /\ x C_ dom _Made ) -> ( ( _Made " x ) C_ Fin <-> A. y e. x ( _Made ` y ) e. Fin ) )
21 11 19 20 sylancr 
 |-  ( x e. _om -> ( ( _Made " x ) C_ Fin <-> A. y e. x ( _Made ` y ) e. Fin ) )
22 21 biimpar 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> ( _Made " x ) C_ Fin )
23 unifi 
 |-  ( ( ( _Made " x ) e. Fin /\ ( _Made " x ) C_ Fin ) -> U. ( _Made " x ) e. Fin )
24 15 22 23 syl2anc 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> U. ( _Made " x ) e. Fin )
25 pwfi 
 |-  ( U. ( _Made " x ) e. Fin <-> ~P U. ( _Made " x ) e. Fin )
26 24 25 sylib 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> ~P U. ( _Made " x ) e. Fin )
27 xpfi 
 |-  ( ( ~P U. ( _Made " x ) e. Fin /\ ~P U. ( _Made " x ) e. Fin ) -> ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) e. Fin )
28 26 26 27 syl2anc 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) e. Fin )
29 vex 
 |-  x e. _V
30 29 funimaex 
 |-  ( Fun _Made -> ( _Made " x ) e. _V )
31 11 30 ax-mp 
 |-  ( _Made " x ) e. _V
32 31 uniex 
 |-  U. ( _Made " x ) e. _V
33 32 pwex 
 |-  ~P U. ( _Made " x ) e. _V
34 33 33 xpex 
 |-  ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) e. _V
35 scutf 
 |-  |s : < No
36 ffun 
 |-  ( |s : < No -> Fun |s )
37 35 36 ax-mp 
 |-  Fun |s
38 imadomg 
 |-  ( ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) e. _V -> ( Fun |s -> ( |s " ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) ) ~<_ ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) ) )
39 34 37 38 mp2 
 |-  ( |s " ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) ) ~<_ ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) )
40 domfi 
 |-  ( ( ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) e. Fin /\ ( |s " ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) ) ~<_ ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) ) -> ( |s " ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) ) e. Fin )
41 28 39 40 sylancl 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> ( |s " ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) ) e. Fin )
42 8 41 eqeltrd 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> ( _Made ` x ) e. Fin )
43 42 ex 
 |-  ( x e. _om -> ( A. y e. x ( _Made ` y ) e. Fin -> ( _Made ` x ) e. Fin ) )
44 2 4 43 omsinds 
 |-  ( A e. _om -> ( _Made ` A ) e. Fin )