Metamath Proof Explorer

Theorem onsupintrab

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

		Ref	Expression
	Assertion	onsupintrab	\|- ( ( A C_ On /\ A e. V ) -> sup ( A , On , _E ) = \|^\| { x e. On \| A. y e. A y C_ x } )

Proof

Step	Hyp	Ref	Expression
1		onsupuni	\|- ( ( A C_ On /\ A e. V ) -> sup ( A , On , _E ) = U. A )
2		onuniintrab	\|- ( ( A C_ On /\ A e. V ) -> U. A = \|^\| { x e. On \| A. y e. A y C_ x } )
3	1 2	eqtrd	\|- ( ( A C_ On /\ A e. V ) -> sup ( A , On , _E ) = \|^\| { x e. On \| A. y e. A y C_ x } )

Step

Hyp

Ref

Expression

onsupuni

 |-  ( ( A C_ On /\ A e. V ) -> sup ( A , On , _E ) = U. A )

onuniintrab

 |-  ( ( A C_ On /\ A e. V ) -> U. A = |^| { x e. On | A. y e. A y C_ x } )

1 2

eqtrd

 |-  ( ( A C_ On /\ A e. V ) -> sup ( A , On , _E ) = |^| { x e. On | A. y e. A y C_ x } )