Theorem oninfunirab

Description: The infimum of a non-empty class of ordinals is the union of every ordinal less-than-or-equal to every element of that class. (Contributed by RP, 23-Jan-2025)

	Ref	Expression
Assertion	oninfunirab	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to inf\left(A,\mathrm{On},\mathrm{E}\right)=\bigcup \left\{x\in \mathrm{On}|\forall y\in Ax\subseteq y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		oninfint	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to inf\left(A,\mathrm{On},\mathrm{E}\right)=\bigcap A$$
2		onintunirab	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to \bigcap A=\bigcup \left\{x\in \mathrm{On}|\forall y\in Ax\subseteq y\right\}$$
3	1 2	eqtrd	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to inf\left(A,\mathrm{On},\mathrm{E}\right)=\bigcup \left\{x\in \mathrm{On}|\forall y\in Ax\subseteq y\right\}$$