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 ( 𝐴 ⊆ 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 𝐴 )