Metamath Proof Explorer

Theorem onsuplub

Description: The supremum of a set of ordinals is the least upper bound. (Contributed by RP, 27-Jan-2025)

Ref Expression
Assertion onsuplub 
|- ( ( ( A C_ On /\ A e. V ) /\ B e. On ) -> ( B e. U. A <-> E. z e. A B e. z ) )

Proof

Step Hyp Ref Expression
1 eluni2 
 |-  ( B e. U. A <-> E. z e. A B e. z )
2 1 a1i 
 |-  ( ( ( A C_ On /\ A e. V ) /\ B e. On ) -> ( B e. U. A <-> E. z e. A B e. z ) )