Theorem onsupeqmax

Description: Condition when the supremum of a set of ordinals is the maximum element of that set. (Contributed by RP, 24-Jan-2025)

	Ref	Expression
Assertion	onsupeqmax	$$⊢\left(A\subseteq \mathrm{On}\wedge A\in V\right)\to \left(\exists x\in A\forall y\in Ay\subseteq x\leftrightarrow \bigcup A\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		unielid	$$⊢\bigcup A\in A\leftrightarrow \exists x\in A\forall y\in Ay\subseteq x$$
2	1	a1i	$$⊢\left(A\subseteq \mathrm{On}\wedge A\in V\right)\to \left(\bigcup A\in A\leftrightarrow \exists x\in A\forall y\in Ay\subseteq x\right)$$
3	2	bicomd	$$⊢\left(A\subseteq \mathrm{On}\wedge A\in V\right)\to \left(\exists x\in A\forall y\in Ay\subseteq x\leftrightarrow \bigcup A\in A\right)$$