Theorem iununi

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

	Ref	Expression
Assertion	iununi	$$⊢\left(B=\varnothing \to A=\varnothing \right)\leftrightarrow A\cup \bigcup B=\bigcup _{x\in B}\left(A\cup x\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ne	$$⊢B\ne \varnothing \leftrightarrow \neg B=\varnothing$$
2		iunconst	$$⊢B\ne \varnothing \to \bigcup _{x\in B}A=A$$
3	1 2	sylbir	$$⊢\neg B=\varnothing \to \bigcup _{x\in B}A=A$$
4		iun0	$$⊢\bigcup _{x\in B}\varnothing =\varnothing$$
5		id	$$⊢A=\varnothing \to A=\varnothing$$
6	5	iuneq2d	$$⊢A=\varnothing \to \bigcup _{x\in B}A=\bigcup _{x\in B}\varnothing$$
7	4 6 5	3eqtr4a	$$⊢A=\varnothing \to \bigcup _{x\in B}A=A$$
8	3 7	ja	$$⊢\left(B=\varnothing \to A=\varnothing \right)\to \bigcup _{x\in B}A=A$$
9	8	eqcomd	$$⊢\left(B=\varnothing \to A=\varnothing \right)\to A=\bigcup _{x\in B}A$$
10	9	uneq1d	$$⊢\left(B=\varnothing \to A=\varnothing \right)\to A\cup \bigcup _{x\in B}x=\bigcup _{x\in B}A\cup \bigcup _{x\in B}x$$
11		uniiun	$$⊢\bigcup B=\bigcup _{x\in B}x$$
12	11	uneq2i	$$⊢A\cup \bigcup B=A\cup \bigcup _{x\in B}x$$
13		iunun	$$⊢\bigcup _{x\in B}\left(A\cup x\right)=\bigcup _{x\in B}A\cup \bigcup _{x\in B}x$$
14	10 12 13	3eqtr4g	$$⊢\left(B=\varnothing \to A=\varnothing \right)\to A\cup \bigcup B=\bigcup _{x\in B}\left(A\cup x\right)$$
15		unieq	$$⊢B=\varnothing \to \bigcup B=\bigcup \varnothing$$
16		uni0	$$⊢\bigcup \varnothing =\varnothing$$
17	15 16	eqtrdi	$$⊢B=\varnothing \to \bigcup B=\varnothing$$
18	17	uneq2d	$$⊢B=\varnothing \to A\cup \bigcup B=A\cup \varnothing$$
19		un0	$$⊢A\cup \varnothing =A$$
20	18 19	eqtrdi	$$⊢B=\varnothing \to A\cup \bigcup B=A$$
21		iuneq1	$$⊢B=\varnothing \to \bigcup _{x\in B}\left(A\cup x\right)=\bigcup _{x\in \varnothing }\left(A\cup x\right)$$
22		0iun	$$⊢\bigcup _{x\in \varnothing }\left(A\cup x\right)=\varnothing$$
23	21 22	eqtrdi	$$⊢B=\varnothing \to \bigcup _{x\in B}\left(A\cup x\right)=\varnothing$$
24	20 23	eqeq12d	$$⊢B=\varnothing \to \left(A\cup \bigcup B=\bigcup _{x\in B}\left(A\cup x\right)\leftrightarrow A=\varnothing \right)$$
25	24	biimpcd	$$⊢A\cup \bigcup B=\bigcup _{x\in B}\left(A\cup x\right)\to \left(B=\varnothing \to A=\varnothing \right)$$
26	14 25	impbii	$$⊢\left(B=\varnothing \to A=\varnothing \right)\leftrightarrow A\cup \bigcup B=\bigcup _{x\in B}\left(A\cup x\right)$$