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

Metamath Proof Explorer

Theorem ssonunii

Description: The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of Enderton p. 193. (Contributed by NM, 20-Sep-2003)

		Ref	Expression
	Hypothesis	ssonuni.1	$⊢ A \in V$
	Assertion	ssonunii	$⊢ A \subseteq On \to ⋃ A \in On$

Step	Hyp	Ref	Expression
1		ssonuni.1	$⊢ A \in V$
2		ssonuni	$⊢ A \in V \to (A \subseteq On \to ⋃ A \in On)$
3	1 2	ax-mp	$⊢ A \subseteq On \to ⋃ A \in On$