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	⊢ ( 𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssorduni	⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )
2		ssid	⊢ ∪ 𝐴 ⊆ ∪ 𝐴
3		ordunisssuc	⊢ ( ( 𝐴 ⊆ On ∧ Ord ∪ 𝐴 ) → ( ∪ 𝐴 ⊆ ∪ 𝐴 ↔ 𝐴 ⊆ suc ∪ 𝐴 ) )
4	2 3	mpbii	⊢ ( ( 𝐴 ⊆ On ∧ Ord ∪ 𝐴 ) → 𝐴 ⊆ suc ∪ 𝐴 )
5	1 4	mpdan	⊢ ( 𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴 )