Theorem oninfex2

Description: The infimum of a non-empty class of ordinals exists. (Contributed by RP, 23-Jan-2025)

	Ref	Expression
Assertion	oninfex2	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to \bigcup \left\{x\in \mathrm{On}|\forall y\in Ax\subseteq y\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		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\}$$
2		intex	$$⊢A\ne \varnothing \leftrightarrow \bigcap A\in \mathrm{V}$$
3	2	biimpi	$$⊢A\ne \varnothing \to \bigcap A\in \mathrm{V}$$
4	3	adantl	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to \bigcap A\in \mathrm{V}$$
5	1 4	eqeltrrd	$$⊢\left(A\subseteq \mathrm{On}\wedge A\ne \varnothing \right)\to \bigcup \left\{x\in \mathrm{On}|\forall y\in Ax\subseteq y\right\}\in \mathrm{V}$$