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 \mathrm{On}\to A\subseteq \mathrm{suc}\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		ssorduni	$$⊢A\subseteq \mathrm{On}\to \mathrm{Ord}\bigcup A$$
2		ssid	$$⊢\bigcup A\subseteq \bigcup A$$
3		ordunisssuc	$$⊢\left(A\subseteq \mathrm{On}\wedge \mathrm{Ord}\bigcup A\right)\to \left(\bigcup A\subseteq \bigcup A\leftrightarrow A\subseteq \mathrm{suc}\bigcup A\right)$$
4	2 3	mpbii	$$⊢\left(A\subseteq \mathrm{On}\wedge \mathrm{Ord}\bigcup A\right)\to A\subseteq \mathrm{suc}\bigcup A$$
5	1 4	mpdan	$$⊢A\subseteq \mathrm{On}\to A\subseteq \mathrm{suc}\bigcup A$$