Metamath Proof Explorer

Theorem oninfcl2

Description: The infimum of a non-empty class of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025)

Ref Expression
Assertion oninfcl2 
|- ( ( A C_ On /\ A =/= (/) ) -> U. { x e. On | A. y e. A x C_ y } e. On )

Proof

Step Hyp Ref Expression
1 onintunirab 
 |-  ( ( A C_ On /\ A =/= (/) ) -> |^| A = U. { x e. On | A. y e. A x C_ y } )
2 oninton 
 |-  ( ( A C_ On /\ A =/= (/) ) -> |^| A e. On )
3 1 2 eqeltrrd 
 |-  ( ( A C_ On /\ A =/= (/) ) -> U. { x e. On | A. y e. A x C_ y } e. On )