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 ( 𝐴 ∈ ω → ( M ‘ 𝐴 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑥 = 𝑦 → ( M ‘ 𝑥 ) = ( M ‘ 𝑦 ) )
2 1 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( M ‘ 𝑥 ) ∈ Fin ↔ ( M ‘ 𝑦 ) ∈ Fin ) )
3 fveq2 ⊢ ( 𝑥 = 𝐴 → ( M ‘ 𝑥 ) = ( M ‘ 𝐴 ) )
4 3 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( M ‘ 𝑥 ) ∈ Fin ↔ ( M ‘ 𝐴 ) ∈ Fin ) )
5 nnon ⊢ ( 𝑥 ∈ ω → 𝑥 ∈ On )
6 madeval ⊢ ( 𝑥 ∈ On → ( M ‘ 𝑥 ) = ( |s “ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ) )
7 5 6 syl ⊢ ( 𝑥 ∈ ω → ( M ‘ 𝑥 ) = ( |s “ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ) )
8 7 adantr ⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → ( M ‘ 𝑥 ) = ( |s “ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ) )
9 cutsf ⊢ |s : <<s ⟶ No
10 ffun ⊢ ( |s : <<s ⟶ No → Fun |s )
11 9 10 ax-mp ⊢ Fun |s
12 madef ⊢ M : On ⟶ 𝒫 No
13 ffun ⊢ ( M : On ⟶ 𝒫 No → Fun M )
14 12 13 ax-mp ⊢ Fun M
15 nnfi ⊢ ( 𝑥 ∈ ω → 𝑥 ∈ Fin )
16 imafi ⊢ ( ( Fun M ∧ 𝑥 ∈ Fin ) → ( M “ 𝑥 ) ∈ Fin )
17 14 15 16 sylancr ⊢ ( 𝑥 ∈ ω → ( M “ 𝑥 ) ∈ Fin )
18 17 adantr ⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → ( M “ 𝑥 ) ∈ Fin )
19 onss ⊢ ( 𝑥 ∈ On → 𝑥 ⊆ On )
20 5 19 syl ⊢ ( 𝑥 ∈ ω → 𝑥 ⊆ On )
21 12 fdmi ⊢ dom M = On
22 20 21 sseqtrrdi ⊢ ( 𝑥 ∈ ω → 𝑥 ⊆ dom M )
23 funimass4 ⊢ ( ( Fun M ∧ 𝑥 ⊆ dom M ) → ( ( M “ 𝑥 ) ⊆ Fin ↔ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) )
24 14 22 23 sylancr ⊢ ( 𝑥 ∈ ω → ( ( M “ 𝑥 ) ⊆ Fin ↔ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) )
25 24 biimpar ⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → ( M “ 𝑥 ) ⊆ Fin )
26 unifi ⊢ ( ( ( M “ 𝑥 ) ∈ Fin ∧ ( M “ 𝑥 ) ⊆ Fin ) → ∪ ( M “ 𝑥 ) ∈ Fin )
27 18 25 26 syl2anc ⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → ∪ ( M “ 𝑥 ) ∈ Fin )
28 pwfi ⊢ ( ∪ ( M “ 𝑥 ) ∈ Fin ↔ 𝒫 ∪ ( M “ 𝑥 ) ∈ Fin )
29 27 28 sylib ⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → 𝒫 ∪ ( M “ 𝑥 ) ∈ Fin )
30 xpfi ⊢ ( ( 𝒫 ∪ ( M “ 𝑥 ) ∈ Fin ∧ 𝒫 ∪ ( M “ 𝑥 ) ∈ Fin ) → ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ∈ Fin )
31 29 29 30 syl2anc ⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ∈ Fin )
32 imafi ⊢ ( ( Fun |s ∧ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ∈ Fin ) → ( |s “ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ) ∈ Fin )
33 11 31 32 sylancr ⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → ( |s “ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ) ∈ Fin )
34 8 33 eqeltrd ⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → ( M ‘ 𝑥 ) ∈ Fin )
35 34 ex ⊢ ( 𝑥 ∈ ω → ( ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin → ( M ‘ 𝑥 ) ∈ Fin ) )
36 2 4 35 omsinds ⊢ ( 𝐴 ∈ ω → ( M ‘ 𝐴 ) ∈ Fin )