Theorem onuniintrab

Description: The union of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. Closed form of uniordint . (Contributed by RP, 28-Jan-2025)

	Ref	Expression
Assertion	onuniintrab	$$⊢\left(A\subseteq \mathrm{On}\wedge A\in V\right)\to \bigcup A=\bigcap \left\{x\in \mathrm{On}|\forall y\in Ay\subseteq x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ssonuni	$$⊢A\in V\to \left(A\subseteq \mathrm{On}\to \bigcup A\in \mathrm{On}\right)$$
2	1	impcom	$$⊢\left(A\subseteq \mathrm{On}\wedge A\in V\right)\to \bigcup A\in \mathrm{On}$$
3		intmin	$$⊢\bigcup A\in \mathrm{On}\to \bigcap \left\{x\in \mathrm{On}|\bigcup A\subseteq x\right\}=\bigcup A$$
4		unissb	$$⊢\bigcup A\subseteq x\leftrightarrow \forall y\in Ay\subseteq x$$
5	4	rabbii	$$⊢\left\{x\in \mathrm{On}|\bigcup A\subseteq x\right\}=\left\{x\in \mathrm{On}|\forall y\in Ay\subseteq x\right\}$$
6	5	inteqi	$$⊢\bigcap \left\{x\in \mathrm{On}|\bigcup A\subseteq x\right\}=\bigcap \left\{x\in \mathrm{On}|\forall y\in Ay\subseteq x\right\}$$
7	3 6	eqtr3di	$$⊢\bigcup A\in \mathrm{On}\to \bigcup A=\bigcap \left\{x\in \mathrm{On}|\forall y\in Ay\subseteq x\right\}$$
8	2 7	syl	$$⊢\left(A\subseteq \mathrm{On}\wedge A\in V\right)\to \bigcup A=\bigcap \left\{x\in \mathrm{On}|\forall y\in Ay\subseteq x\right\}$$