Theorem onsupcl3

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

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

Proof

Step	Hyp	Ref	Expression
1		onuniintrab	|- ( ( A C_ On /\ A e. V ) -> U. A = |^| { x e. On | A. y e. A y C_ x } )
2		ssonuni	|- ( A e. V -> ( A C_ On -> U. A e. On ) )
3	2	impcom	|- ( ( A C_ On /\ A e. V ) -> U. A e. On )
4	1 3	eqeltrrd	|- ( ( A C_ On /\ A e. V ) -> |^| { x e. On | A. y e. A y C_ x } e. On )