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 ∈ ω → M ⁡ A ∈ Fin

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ x = y → M ⁡ x = M ⁡ y
2 1 eleq1d ⊢ x = y → M ⁡ x ∈ Fin ↔ M ⁡ y ∈ Fin
3 fveq2 ⊢ x = A → M ⁡ x = M ⁡ A
4 3 eleq1d ⊢ x = A → M ⁡ x ∈ Fin ↔ M ⁡ A ∈ Fin
5 nnon ⊢ x ∈ ω → x ∈ On
6 madeval ⊢ x ∈ On → M ⁡ x = | s 𝒫 ⋃ M x × 𝒫 ⋃ M x
7 5 6 syl ⊢ x ∈ ω → M ⁡ x = | s 𝒫 ⋃ M x × 𝒫 ⋃ M x
8 7 adantr ⊢ x ∈ ω ∧ ∀ y ∈ x M ⁡ y ∈ Fin → M ⁡ x = | s 𝒫 ⋃ M x × 𝒫 ⋃ M x
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 ⊢ x ∈ ω → x ∈ Fin
16 imafi ⊢ Fun ⁡ M ∧ x ∈ Fin → M x ∈ Fin
17 14 15 16 sylancr ⊢ x ∈ ω → M x ∈ Fin
18 17 adantr ⊢ x ∈ ω ∧ ∀ y ∈ x M ⁡ y ∈ Fin → M x ∈ Fin
19 onss ⊢ x ∈ On → x ⊆ On
20 5 19 syl ⊢ x ∈ ω → x ⊆ On
21 12 fdmi ⊢ dom ⁡ M = On
22 20 21 sseqtrrdi ⊢ x ∈ ω → x ⊆ dom ⁡ M
23 funimass4 ⊢ Fun ⁡ M ∧ x ⊆ dom ⁡ M → M x ⊆ Fin ↔ ∀ y ∈ x M ⁡ y ∈ Fin
24 14 22 23 sylancr ⊢ x ∈ ω → M x ⊆ Fin ↔ ∀ y ∈ x M ⁡ y ∈ Fin
25 24 biimpar ⊢ x ∈ ω ∧ ∀ y ∈ x M ⁡ y ∈ Fin → M x ⊆ Fin
26 unifi ⊢ M x ∈ Fin ∧ M x ⊆ Fin → ⋃ M x ∈ Fin
27 18 25 26 syl2anc ⊢ x ∈ ω ∧ ∀ y ∈ x M ⁡ y ∈ Fin → ⋃ M x ∈ Fin
28 pwfi ⊢ ⋃ M x ∈ Fin ↔ 𝒫 ⋃ M x ∈ Fin
29 27 28 sylib ⊢ x ∈ ω ∧ ∀ y ∈ x M ⁡ y ∈ Fin → 𝒫 ⋃ M x ∈ Fin
30 xpfi ⊢ 𝒫 ⋃ M x ∈ Fin ∧ 𝒫 ⋃ M x ∈ Fin → 𝒫 ⋃ M x × 𝒫 ⋃ M x ∈ Fin
31 29 29 30 syl2anc ⊢ x ∈ ω ∧ ∀ y ∈ x M ⁡ y ∈ Fin → 𝒫 ⋃ M x × 𝒫 ⋃ M x ∈ Fin
32 imafi ⊢ Fun ⁡ | s ∧ 𝒫 ⋃ M x × 𝒫 ⋃ M x ∈ Fin → | s 𝒫 ⋃ M x × 𝒫 ⋃ M x ∈ Fin
33 11 31 32 sylancr ⊢ x ∈ ω ∧ ∀ y ∈ x M ⁡ y ∈ Fin → | s 𝒫 ⋃ M x × 𝒫 ⋃ M x ∈ Fin
34 8 33 eqeltrd ⊢ x ∈ ω ∧ ∀ y ∈ x M ⁡ y ∈ Fin → M ⁡ x ∈ Fin
35 34 ex ⊢ x ∈ ω → ∀ y ∈ x M ⁡ y ∈ Fin → M ⁡ x ∈ Fin
36 2 4 35 omsinds ⊢ A ∈ ω → M ⁡ A ∈ Fin