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 C_ On -> A C_ suc U. A )

Proof

Step	Hyp	Ref	Expression
1		ssorduni	|- ( A C_ On -> Ord U. A )
2		ssid	|- U. A C_ U. A
3		ordunisssuc	|- ( ( A C_ On /\ Ord U. A ) -> ( U. A C_ U. A <-> A C_ suc U. A ) )
4	2 3	mpbii	|- ( ( A C_ On /\ Ord U. A ) -> A C_ suc U. A )
5	1 4	mpdan	|- ( A C_ On -> A C_ suc U. A )