nnuni

Description: The union of a finite ordinal is a finite ordinal. (Contributed by Scott Fenton, 17-Oct-2024)

		Ref	Expression
	Assertion	nnuni	$⊢ A \in ω \to ⋃ A \in ω$

Step	Hyp	Ref	Expression
1		nn0suc	$⊢ A \in ω \to (A = \emptyset \lor \exists x \in ω A = suc x)$
2		unieq	$⊢ A = \emptyset \to ⋃ A = ⋃ \emptyset$
3		uni0	$⊢ ⋃ \emptyset = \emptyset$
4	2 3	eqtrdi	$⊢ A = \emptyset \to ⋃ A = \emptyset$
5		peano1	$⊢ \emptyset \in ω$
6	4 5	eqeltrdi	$⊢ A = \emptyset \to ⋃ A \in ω$
7		nnord	$⊢ x \in ω \to Ord x$
8		ordunisuc	$⊢ Ord x \to ⋃ suc x = x$
9	7 8	syl	$⊢ x \in ω \to ⋃ suc x = x$
10		id	$⊢ x \in ω \to x \in ω$
11	9 10	eqeltrd	$⊢ x \in ω \to ⋃ suc x \in ω$
12		unieq	$⊢ A = suc x \to ⋃ A = ⋃ suc x$
13	12	eleq1d	$⊢ A = suc x \to (⋃ A \in ω \leftrightarrow ⋃ suc x \in ω)$
14	11 13	syl5ibrcom	$⊢ x \in ω \to (A = suc x \to ⋃ A \in ω)$
15	14	rexlimiv	$⊢ \exists x \in ω A = suc x \to ⋃ A \in ω$
16	6 15	jaoi	$⊢ (A = \emptyset \lor \exists x \in ω A = suc x) \to ⋃ A \in ω$
17	1 16	syl	$⊢ A \in ω \to ⋃ A \in ω$

Metamath Proof Explorer