Metamath Proof Explorer

Theorem onsupex3

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

Ref Expression
Assertion onsupex3 
|- ( ( A C_ On /\ A e. V ) -> |^| { x e. On | A. y e. A y C_ x } e. _V )

Proof

Step Hyp Ref Expression
1 onsupcl3 
 |-  ( ( A C_ On /\ A e. V ) -> |^| { x e. On | A. y e. A y C_ x } e. On )
2 1 elexd 
 |-  ( ( A C_ On /\ A e. V ) -> |^| { x e. On | A. y e. A y C_ x } e. _V )