Theorem onsupintrab2

Description: The supremum of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. (Contributed by RP, 23-Jan-2025)

	Ref	Expression
Assertion	onsupintrab2	|- ( A e. ~P On -> sup ( A , On , _E ) = |^| { x e. On | A. y e. A y C_ x } )

Proof

Step	Hyp	Ref	Expression
1		elpwb	|- ( A e. ~P On <-> ( A e. _V /\ A C_ On ) )
2		onsupintrab	|- ( ( A C_ On /\ A e. _V ) -> sup ( A , On , _E ) = |^| { x e. On | A. y e. A y C_ x } )
3	2	ancoms	|- ( ( A e. _V /\ A C_ On ) -> sup ( A , On , _E ) = |^| { x e. On | A. y e. A y C_ x } )
4	1 3	sylbi	|- ( A e. ~P On -> sup ( A , On , _E ) = |^| { x e. On | A. y e. A y C_ x } )