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 \subseteq On \land A \in V) \land (B \in On \land \forall z \in A z \subseteq B)) \to ⋃ A \subseteq B$

Step	Hyp	Ref	Expression
1		simprr	$⊢ ((A \subseteq On \land A \in V) \land (B \in On \land \forall z \in A z \subseteq B)) \to \forall z \in A z \subseteq B$
2		unissb	$⊢ ⋃ A \subseteq B \leftrightarrow \forall z \in A z \subseteq B$
3	1 2	sylibr	$⊢ ((A \subseteq On \land A \in V) \land (B \in On \land \forall z \in A z \subseteq B)) \to ⋃ A \subseteq B$