Metamath Proof Explorer

Theorem madefi

Description: The made set of an ordinal natural is finite. (Contributed by Scott Fenton, 20-Aug-2025) (Proof shortened by Vincent Gonzalez, 19-Aug-2026)

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 cutsf 
 |-  |s : < No
10 ffun 
 |-  ( |s : < No -> Fun |s )
11 9 10 ax-mp 
 |-  Fun |s
12 madef 
 |-  _Made : On --> ~P No
13 ffun 
 |-  ( _Made : On --> ~P No -> Fun _Made )
14 12 13 ax-mp 
 |-  Fun _Made
15 nnfi 
 |-  ( x e. _om -> x e. Fin )
16 imafi 
 |-  ( ( Fun _Made /\ x e. Fin ) -> ( _Made " x ) e. Fin )
17 14 15 16 sylancr 
 |-  ( x e. _om -> ( _Made " x ) e. Fin )
18 17 adantr 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> ( _Made " x ) e. Fin )
19 onss 
 |-  ( x e. On -> x C_ On )
20 5 19 syl 
 |-  ( x e. _om -> x C_ On )
21 12 fdmi 
 |-  dom _Made = On
22 20 21 sseqtrrdi 
 |-  ( x e. _om -> x C_ dom _Made )
23 funimass4 
 |-  ( ( Fun _Made /\ x C_ dom _Made ) -> ( ( _Made " x ) C_ Fin <-> A. y e. x ( _Made ` y ) e. Fin ) )
24 14 22 23 sylancr 
 |-  ( x e. _om -> ( ( _Made " x ) C_ Fin <-> A. y e. x ( _Made ` y ) e. Fin ) )
25 24 biimpar 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> ( _Made " x ) C_ Fin )
26 unifi 
 |-  ( ( ( _Made " x ) e. Fin /\ ( _Made " x ) C_ Fin ) -> U. ( _Made " x ) e. Fin )
27 18 25 26 syl2anc 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> U. ( _Made " x ) e. Fin )
28 pwfi 
 |-  ( U. ( _Made " x ) e. Fin <-> ~P U. ( _Made " x ) e. Fin )
29 27 28 sylib 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> ~P U. ( _Made " x ) e. Fin )
30 xpfi 
 |-  ( ( ~P U. ( _Made " x ) e. Fin /\ ~P U. ( _Made " x ) e. Fin ) -> ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) e. Fin )
31 29 29 30 syl2anc 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) e. Fin )
32 imafi 
 |-  ( ( Fun |s /\ ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) e. Fin ) -> ( |s " ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) ) e. Fin )
33 11 31 32 sylancr 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> ( |s " ( ~P U. ( _Made " x ) X. ~P U. ( _Made " x ) ) ) e. Fin )
34 8 33 eqeltrd 
 |-  ( ( x e. _om /\ A. y e. x ( _Made ` y ) e. Fin ) -> ( _Made ` x ) e. Fin )
35 34 ex 
 |-  ( x e. _om -> ( A. y e. x ( _Made ` y ) e. Fin -> ( _Made ` x ) e. Fin ) )
36 2 4 35 omsinds 
 |-  ( A e. _om -> ( _Made ` A ) e. Fin )