Metamath Proof Explorer

Theorem onsupuni2

Description: The supremum of a set of ordinals is the union of that set. (Contributed by RP, 22-Jan-2025)

Ref Expression
Assertion onsupuni2 
|- ( A e. ~P On -> sup ( A , On , _E ) = U. A )

Proof

Step Hyp Ref Expression
1 elpwb 
 |-  ( A e. ~P On <-> ( A e. _V /\ A C_ On ) )
2 onsupuni 
 |-  ( ( A C_ On /\ A e. _V ) -> sup ( A , On , _E ) = U. A )
3 2 ancoms 
 |-  ( ( A e. _V /\ A C_ On ) -> sup ( A , On , _E ) = U. A )
4 1 3 sylbi 
 |-  ( A e. ~P On -> sup ( A , On , _E ) = U. A )