Theorem uniordint

Description: The union of a set of ordinals is equal to the intersection of its upper bounds. Problem 2.5(ii) of BellMachover p. 471. (Contributed by NM, 20-Sep-2003)

	Ref	Expression
Hypothesis	uniordint.1	$$⊢A\in \mathrm{V}$$
Assertion	uniordint	$$⊢A\subseteq \mathrm{On}\to \bigcup A=\bigcap \left\{x\in \mathrm{On}|\forall y\in Ay\subseteq x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		uniordint.1	$$⊢A\in \mathrm{V}$$
2	1	ssonunii	$$⊢A\subseteq \mathrm{On}\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	$$⊢A\subseteq \mathrm{On}\to \bigcup A=\bigcap \left\{x\in \mathrm{On}|\forall y\in Ay\subseteq x\right\}$$