Theorem iinuni

Description: A relationship involving union and indexed intersection. Exercise 23 of Enderton p. 33. (Contributed by NM, 25-Nov-2003) (Proof shortened by Mario Carneiro, 17-Nov-2016)

	Ref	Expression
Assertion	iinuni	$$⊢A\cup \bigcap B=\bigcap _{x\in B}\left(A\cup x\right)$$

Proof

Step	Hyp	Ref	Expression
1		r19.32v	$$⊢\forall x\in B\left(y\in A\vee y\in x\right)\leftrightarrow \left(y\in A\vee \forall x\in By\in x\right)$$
2		elun	$$⊢y\in \left(A\cup x\right)\leftrightarrow \left(y\in A\vee y\in x\right)$$
3	2	ralbii	$$⊢\forall x\in By\in \left(A\cup x\right)\leftrightarrow \forall x\in B\left(y\in A\vee y\in x\right)$$
4		vex	$$⊢y\in \mathrm{V}$$
5	4	elint2	$$⊢y\in \bigcap B\leftrightarrow \forall x\in By\in x$$
6	5	orbi2i	$$⊢\left(y\in A\vee y\in \bigcap B\right)\leftrightarrow \left(y\in A\vee \forall x\in By\in x\right)$$
7	1 3 6	3bitr4ri	$$⊢\left(y\in A\vee y\in \bigcap B\right)\leftrightarrow \forall x\in By\in \left(A\cup x\right)$$
8	7	abbii	$$⊢\left\{y|\left(y\in A\vee y\in \bigcap B\right)\right\}=\left\{y|\forall x\in By\in \left(A\cup x\right)\right\}$$
9		df-un	$$⊢A\cup \bigcap B=\left\{y|\left(y\in A\vee y\in \bigcap B\right)\right\}$$
10		df-iin	$$⊢\bigcap _{x\in B}\left(A\cup x\right)=\left\{y|\forall x\in By\in \left(A\cup x\right)\right\}$$
11	8 9 10	3eqtr4i	$$⊢A\cup \bigcap B=\bigcap _{x\in B}\left(A\cup x\right)$$