Metamath Proof Explorer

Theorem onsupcl2

Description: The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025)

Ref Expression
Assertion onsupcl2 
|- ( A e. ~P On -> U. A e. On )

Proof

Step Hyp Ref Expression
1 elpwb 
 |-  ( A e. ~P On <-> ( A e. _V /\ A C_ On ) )
2 ssonuni 
 |-  ( A e. _V -> ( A C_ On -> U. A e. On ) )
3 2 imp 
 |-  ( ( A e. _V /\ A C_ On ) -> U. A e. On )
4 1 3 sylbi 
 |-  ( A e. ~P On -> U. A e. On )