Theorem madefi

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

	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		madef	⊢ M : On ⟶ 𝒫 No
10		ffun	⊢ ( M : On ⟶ 𝒫 No → Fun M )
11	9 10	ax-mp	⊢ Fun M
12		nnfi	⊢ ( 𝑥 ∈ ω → 𝑥 ∈ Fin )
13		imafi	⊢ ( ( Fun M ∧ 𝑥 ∈ Fin ) → ( M “ 𝑥 ) ∈ Fin )
14	11 12 13	sylancr	⊢ ( 𝑥 ∈ ω → ( M “ 𝑥 ) ∈ Fin )
15	14	adantr	⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → ( M “ 𝑥 ) ∈ Fin )
16		onss	⊢ ( 𝑥 ∈ On → 𝑥 ⊆ On )
17	5 16	syl	⊢ ( 𝑥 ∈ ω → 𝑥 ⊆ On )
18	9	fdmi	⊢ dom M = On
19	17 18	sseqtrrdi	⊢ ( 𝑥 ∈ ω → 𝑥 ⊆ dom M )
20		funimass4	⊢ ( ( Fun M ∧ 𝑥 ⊆ dom M ) → ( ( M “ 𝑥 ) ⊆ Fin ↔ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) )
21	11 19 20	sylancr	⊢ ( 𝑥 ∈ ω → ( ( M “ 𝑥 ) ⊆ Fin ↔ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) )
22	21	biimpar	⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → ( M “ 𝑥 ) ⊆ Fin )
23		unifi	⊢ ( ( ( M “ 𝑥 ) ∈ Fin ∧ ( M “ 𝑥 ) ⊆ Fin ) → ∪ ( M “ 𝑥 ) ∈ Fin )
24	15 22 23	syl2anc	⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → ∪ ( M “ 𝑥 ) ∈ Fin )
25		pwfi	⊢ ( ∪ ( M “ 𝑥 ) ∈ Fin ↔ 𝒫 ∪ ( M “ 𝑥 ) ∈ Fin )
26	24 25	sylib	⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → 𝒫 ∪ ( M “ 𝑥 ) ∈ Fin )
27		xpfi	⊢ ( ( 𝒫 ∪ ( M “ 𝑥 ) ∈ Fin ∧ 𝒫 ∪ ( M “ 𝑥 ) ∈ Fin ) → ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ∈ Fin )
28	26 26 27	syl2anc	⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ∈ Fin )
29		vex	⊢ 𝑥 ∈ V
30	29	funimaex	⊢ ( Fun M → ( M “ 𝑥 ) ∈ V )
31	11 30	ax-mp	⊢ ( M “ 𝑥 ) ∈ V
32	31	uniex	⊢ ∪ ( M “ 𝑥 ) ∈ V
33	32	pwex	⊢ 𝒫 ∪ ( M “ 𝑥 ) ∈ V
34	33 33	xpex	⊢ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ∈ V
35		scutf	⊢ |s : <<s ⟶ No
36		ffun	⊢ ( |s : <<s ⟶ No → Fun |s )
37	35 36	ax-mp	⊢ Fun |s
38		imadomg	⊢ ( ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ∈ V → ( Fun |s → ( |s “ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ) ≼ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ) )
39	34 37 38	mp2	⊢ ( |s “ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ) ≼ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) )
40		domfi	⊢ ( ( ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ∈ Fin ∧ ( |s “ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ) ≼ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ) → ( |s “ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ) ∈ Fin )
41	28 39 40	sylancl	⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → ( |s “ ( 𝒫 ∪ ( M “ 𝑥 ) × 𝒫 ∪ ( M “ 𝑥 ) ) ) ∈ Fin )
42	8 41	eqeltrd	⊢ ( ( 𝑥 ∈ ω ∧ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) → ( M ‘ 𝑥 ) ∈ Fin )
43	42	ex	⊢ ( 𝑥 ∈ ω → ( ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin → ( M ‘ 𝑥 ) ∈ Fin ) )
44	2 4 43	omsinds	⊢ ( 𝐴 ∈ ω → ( M ‘ 𝐴 ) ∈ Fin )