Metamath Proof Explorer

Theorem onsucunifi

Description: The successor to the union of any non-empty, finite subset of ordinals is the union of the successors of the elements. (Contributed by RP, 12-Feb-2025)

		Ref	Expression
	Assertion	onsucunifi	$⊢ (A \subseteq On \land A \in Fin \land A \neq \emptyset) \to suc ⋃ A = ⋃_{x \in A} suc x$

Proof

Step	Hyp	Ref	Expression
1		ordunifi	$⊢ (A \subseteq On \land A \in Fin \land A \neq \emptyset) \to ⋃ A \in A$
2		suceq	$⊢ x = ⋃ A \to suc x = suc ⋃ A$
3	2	ssiun2s	$⊢ ⋃ A \in A \to suc ⋃ A \subseteq ⋃_{x \in A} suc x$
4	1 3	syl	$⊢ (A \subseteq On \land A \in Fin \land A \neq \emptyset) \to suc ⋃ A \subseteq ⋃_{x \in A} suc x$
5		ssorduni	$⊢ A \subseteq On \to Ord ⋃ A$
6		ordsuci	$⊢ Ord ⋃ A \to Ord suc ⋃ A$
7	5 6	syl	$⊢ A \subseteq On \to Ord suc ⋃ A$
8		onsucuni	$⊢ A \subseteq On \to A \subseteq suc ⋃ A$
9	8	sselda	$⊢ (A \subseteq On \land x \in A) \to x \in suc ⋃ A$
10		ordsucss	$⊢ Ord suc ⋃ A \to (x \in suc ⋃ A \to suc x \subseteq suc ⋃ A)$
11	10	imp	$⊢ (Ord suc ⋃ A \land x \in suc ⋃ A) \to suc x \subseteq suc ⋃ A$
12	7 9 11	syl2an2r	$⊢ (A \subseteq On \land x \in A) \to suc x \subseteq suc ⋃ A$
13	12	iunssd	$⊢ A \subseteq On \to ⋃_{x \in A} suc x \subseteq suc ⋃ A$
14	13	3ad2ant1	$⊢ (A \subseteq On \land A \in Fin \land A \neq \emptyset) \to ⋃_{x \in A} suc x \subseteq suc ⋃ A$
15	4 14	eqssd	$⊢ (A \subseteq On \land A \in Fin \land A \neq \emptyset) \to suc ⋃ A = ⋃_{x \in A} suc x$