Metamath Proof Explorer

Theorem onsupnub

Description: An upper bound of a set of ordinals is not less than the supremum. (Contributed by RP, 27-Jan-2025)

		Ref	Expression
	Assertion	onsupnub	\|- ( ( ( A C_ On /\ A e. V ) /\ ( B e. On /\ A. z e. A z C_ B ) ) -> U. A C_ B )

Step	Hyp	Ref	Expression
1		simprr	\|- ( ( ( A C_ On /\ A e. V ) /\ ( B e. On /\ A. z e. A z C_ B ) ) -> A. z e. A z C_ B )
2		unissb	\|- ( U. A C_ B <-> A. z e. A z C_ B )
3	1 2	sylibr	\|- ( ( ( A C_ On /\ A e. V ) /\ ( B e. On /\ A. z e. A z C_ B ) ) -> U. A C_ B )

Step

Hyp

Ref

Expression

 |-  ( ( ( A C_ On /\ A e. V ) /\ ( B e. On /\ A. z e. A z C_ B ) ) -> A. z e. A z C_ B )

 |-  ( U. A C_ B <-> A. z e. A z C_ B )

1 2

 |-  ( ( ( A C_ On /\ A e. V ) /\ ( B e. On /\ A. z e. A z C_ B ) ) -> U. A C_ B )