madefi

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

		Ref	Expression
	Assertion	madefi	$⊢ A \in ω \to M (A) \in Fin$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ x = y \to M (x) = M (y)$
2	1	eleq1d	$⊢ x = y \to (M (x) \in Fin \leftrightarrow M (y) \in Fin)$
3		fveq2	$⊢ x = A \to M (x) = M (A)$
4	3	eleq1d	$⊢ x = A \to (M (x) \in Fin \leftrightarrow M (A) \in Fin)$
5		nnon	$⊢ x \in ω \to x \in On$
6		madeval	$⊢ x \in On \to M (x) = \|_{s} [𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x]]$
7	5 6	syl	$⊢ x \in ω \to M (x) = \|_{s} [𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x]]$
8	7	adantr	$⊢ (x \in ω \land \forall y \in x M (y) \in Fin) \to M (x) = \|_{s} [𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x]]$
9		madef	$⊢ M : On ⟶ 𝒫 No$
10		ffun	$⊢ M : On ⟶ 𝒫 No \to Fun M$
11	9 10	ax-mp	$⊢ Fun M$
12		nnfi	$⊢ x \in ω \to x \in Fin$
13		imafi	$⊢ (Fun M \land x \in Fin) \to M [x] \in Fin$
14	11 12 13	sylancr	$⊢ x \in ω \to M [x] \in Fin$
15	14	adantr	$⊢ (x \in ω \land \forall y \in x M (y) \in Fin) \to M [x] \in Fin$
16		onss	$⊢ x \in On \to x \subseteq On$
17	5 16	syl	$⊢ x \in ω \to x \subseteq On$
18	9	fdmi	$⊢ dom M = On$
19	17 18	sseqtrrdi	$⊢ x \in ω \to x \subseteq dom M$
20		funimass4	$⊢ (Fun M \land x \subseteq dom M) \to (M [x] \subseteq Fin \leftrightarrow \forall y \in x M (y) \in Fin)$
21	11 19 20	sylancr	$⊢ x \in ω \to (M [x] \subseteq Fin \leftrightarrow \forall y \in x M (y) \in Fin)$
22	21	biimpar	$⊢ (x \in ω \land \forall y \in x M (y) \in Fin) \to M [x] \subseteq Fin$
23		unifi	$⊢ (M [x] \in Fin \land M [x] \subseteq Fin) \to ⋃ M [x] \in Fin$
24	15 22 23	syl2anc	$⊢ (x \in ω \land \forall y \in x M (y) \in Fin) \to ⋃ M [x] \in Fin$
25		pwfi	$⊢ ⋃ M [x] \in Fin \leftrightarrow 𝒫 ⋃ M [x] \in Fin$
26	24 25	sylib	$⊢ (x \in ω \land \forall y \in x M (y) \in Fin) \to 𝒫 ⋃ M [x] \in Fin$
27		xpfi	$⊢ (𝒫 ⋃ M [x] \in Fin \land 𝒫 ⋃ M [x] \in Fin) \to 𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x] \in Fin$
28	26 26 27	syl2anc	$⊢ (x \in ω \land \forall y \in x M (y) \in Fin) \to 𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x] \in Fin$
29		vex	$⊢ x \in V$
30	29	funimaex	$⊢ Fun M \to M [x] \in V$
31	11 30	ax-mp	$⊢ M [x] \in V$
32	31	uniex	$⊢ ⋃ M [x] \in V$
33	32	pwex	$⊢ 𝒫 ⋃ M [x] \in V$
34	33 33	xpex	$⊢ 𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x] \in V$
35		scutf	$⊢ \|_{s} : ≪_{s} ⟶ No$
36		ffun	$⊢ \|_{s} : ≪_{s} ⟶ No \to Fun \|_{s}$
37	35 36	ax-mp	$⊢ Fun \|_{s}$
38		imadomg	$⊢ 𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x] \in V \to (Fun \|_{s} \to \|_{s} [𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x]] ≼ (𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x]))$
39	34 37 38	mp2	$⊢ \|_{s} [𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x]] ≼ (𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x])$
40		domfi	$⊢ (𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x] \in Fin \land \|_{s} [𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x]] ≼ (𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x])) \to \|_{s} [𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x]] \in Fin$
41	28 39 40	sylancl	$⊢ (x \in ω \land \forall y \in x M (y) \in Fin) \to \|_{s} [𝒫 ⋃ M [x] \times 𝒫 ⋃ M [x]] \in Fin$
42	8 41	eqeltrd	$⊢ (x \in ω \land \forall y \in x M (y) \in Fin) \to M (x) \in Fin$
43	42	ex	$⊢ x \in ω \to (\forall y \in x M (y) \in Fin \to M (x) \in Fin)$
44	2 4 43	omsinds	$⊢ A \in ω \to M (A) \in Fin$

Metamath Proof Explorer

Theorem madefi

Proof