nnunifi

Description: The union (supremum) of a finite set of finite ordinals is a finite ordinal. (Contributed by Stefan O'Rear, 5-Nov-2014)

		Ref	Expression
	Assertion	nnunifi	$⊢ (S \subseteq ω \land S \in Fin) \to ⋃ S \in ω$

Step	Hyp	Ref	Expression
1		unieq	$⊢ S = \emptyset \to ⋃ S = ⋃ \emptyset$
2		uni0	$⊢ ⋃ \emptyset = \emptyset$
3		peano1	$⊢ \emptyset \in ω$
4	2 3	eqeltri	$⊢ ⋃ \emptyset \in ω$
5	1 4	eqeltrdi	$⊢ S = \emptyset \to ⋃ S \in ω$
6	5	adantl	$⊢ ((S \subseteq ω \land S \in Fin) \land S = \emptyset) \to ⋃ S \in ω$
7		simpll	$⊢ ((S \subseteq ω \land S \in Fin) \land S \neq \emptyset) \to S \subseteq ω$
8		omsson	$⊢ ω \subseteq On$
9	7 8	sstrdi	$⊢ ((S \subseteq ω \land S \in Fin) \land S \neq \emptyset) \to S \subseteq On$
10		simplr	$⊢ ((S \subseteq ω \land S \in Fin) \land S \neq \emptyset) \to S \in Fin$
11		simpr	$⊢ ((S \subseteq ω \land S \in Fin) \land S \neq \emptyset) \to S \neq \emptyset$
12		ordunifi	$⊢ (S \subseteq On \land S \in Fin \land S \neq \emptyset) \to ⋃ S \in S$
13	9 10 11 12	syl3anc	$⊢ ((S \subseteq ω \land S \in Fin) \land S \neq \emptyset) \to ⋃ S \in S$
14	7 13	sseldd	$⊢ ((S \subseteq ω \land S \in Fin) \land S \neq \emptyset) \to ⋃ S \in ω$
15	6 14	pm2.61dane	$⊢ (S \subseteq ω \land S \in Fin) \to ⋃ S \in ω$

Metamath Proof Explorer