Theorem iinssiun

Description: An indexed intersection is a subset of the corresponding indexed union. (Contributed by Thierry Arnoux, 31-Dec-2021)

	Ref	Expression
Assertion	iinssiun	$$⊢A\ne \varnothing \to \bigcap _{x\in A}B\subseteq \bigcup _{x\in A}B$$

Proof

Step	Hyp	Ref	Expression
1		r19.2z	$$⊢\left(A\ne \varnothing \wedge \forall x\in Ay\in B\right)\to \exists x\in Ay\in B$$
2	1	ex	$$⊢A\ne \varnothing \to \left(\forall x\in Ay\in B\to \exists x\in Ay\in B\right)$$
3		eliin	$$⊢y\in \mathrm{V}\to \left(y\in \bigcap _{x\in A}B\leftrightarrow \forall x\in Ay\in B\right)$$
4	3	elv	$$⊢y\in \bigcap _{x\in A}B\leftrightarrow \forall x\in Ay\in B$$
5		eliun	$$⊢y\in \bigcup _{x\in A}B\leftrightarrow \exists x\in Ay\in B$$
6	2 4 5	3imtr4g	$$⊢A\ne \varnothing \to \left(y\in \bigcap _{x\in A}B\to y\in \bigcup _{x\in A}B\right)$$
7	6	ssrdv	$$⊢A\ne \varnothing \to \bigcap _{x\in A}B\subseteq \bigcup _{x\in A}B$$