Metamath Proof Explorer

Theorem onsupeqmax

Description: Condition when the supremum of a set of ordinals is the maximum element of that set. (Contributed by RP, 24-Jan-2025)

Ref Expression
Assertion onsupeqmax 
|- ( ( A C_ On /\ A e. V ) -> ( E. x e. A A. y e. A y C_ x <-> U. A e. A ) )

Proof

Step Hyp Ref Expression
1 unielid 
 |-  ( U. A e. A <-> E. x e. A A. y e. A y C_ x )
2 1 a1i 
 |-  ( ( A C_ On /\ A e. V ) -> ( U. A e. A <-> E. x e. A A. y e. A y C_ x ) )
3 2 bicomd 
 |-  ( ( A C_ On /\ A e. V ) -> ( E. x e. A A. y e. A y C_ x <-> U. A e. A ) )