This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssonuni

Description: The union of a set of ordinal numbers is an ordinal number. Theorem 9 of Suppes p. 132. Lemma 2.7 of Schloeder p. 4. (Contributed by NM, 1-Nov-2003)

		Ref	Expression
	Assertion	ssonuni	$⊢ A \in V \to (A \subseteq On \to ⋃ A \in On)$

Proof

Step	Hyp	Ref	Expression
1		ssorduni	$⊢ A \subseteq On \to Ord ⋃ A$
2		uniexg	$⊢ A \in V \to ⋃ A \in V$
3		elong	$⊢ ⋃ A \in V \to (⋃ A \in On \leftrightarrow Ord ⋃ A)$
4	2 3	syl	$⊢ A \in V \to (⋃ A \in On \leftrightarrow Ord ⋃ A)$
5	1 4	imbitrrid	$⊢ A \in V \to (A \subseteq On \to ⋃ A \in On)$