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

Metamath Proof Explorer

Theorem onsucuni

Description: A class of ordinal numbers is a subclass of the successor of its union. Similar to Proposition 7.26 of TakeutiZaring p. 41. (Contributed by NM, 19-Sep-2003)

		Ref	Expression
	Assertion	onsucuni	$⊢ A \subseteq On \to A \subseteq suc ⋃ A$

Proof

Step	Hyp	Ref	Expression
1		ssorduni	$⊢ A \subseteq On \to Ord ⋃ A$
2		ssid	$⊢ ⋃ A \subseteq ⋃ A$
3		ordunisssuc	$⊢ (A \subseteq On \land Ord ⋃ A) \to (⋃ A \subseteq ⋃ A \leftrightarrow A \subseteq suc ⋃ A)$
4	2 3	mpbii	$⊢ (A \subseteq On \land Ord ⋃ A) \to A \subseteq suc ⋃ A$
5	1 4	mpdan	$⊢ A \subseteq On \to A \subseteq suc ⋃ A$