Theorem fipwuni

Description: The set of finite intersections of a set is contained in the powerset of the union of the elements of A . (Contributed by Mario Carneiro, 24-Nov-2013) (Proof shortened by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	fipwuni	$$⊢\mathrm{fi}\left(A\right)\subseteq 𝒫\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		uniexg	$$⊢A\in \mathrm{V}\to \bigcup A\in \mathrm{V}$$
2	1	pwexd	$$⊢A\in \mathrm{V}\to 𝒫\bigcup A\in \mathrm{V}$$
3		pwuni	$$⊢A\subseteq 𝒫\bigcup A$$
4		fiss	$$⊢\left(𝒫\bigcup A\in \mathrm{V}\wedge A\subseteq 𝒫\bigcup A\right)\to \mathrm{fi}\left(A\right)\subseteq \mathrm{fi}\left(𝒫\bigcup A\right)$$
5	2 3 4	sylancl	$$⊢A\in \mathrm{V}\to \mathrm{fi}\left(A\right)\subseteq \mathrm{fi}\left(𝒫\bigcup A\right)$$
6		ssinss1	$$⊢x\subseteq \bigcup A\to x\cap y\subseteq \bigcup A$$
7		vex	$$⊢x\in \mathrm{V}$$
8	7	elpw	$$⊢x\in 𝒫\bigcup A\leftrightarrow x\subseteq \bigcup A$$
9	7	inex1	$$⊢x\cap y\in \mathrm{V}$$
10	9	elpw	$$⊢x\cap y\in 𝒫\bigcup A\leftrightarrow x\cap y\subseteq \bigcup A$$
11	6 8 10	3imtr4i	$$⊢x\in 𝒫\bigcup A\to x\cap y\in 𝒫\bigcup A$$
12	11	adantr	$$⊢\left(x\in 𝒫\bigcup A\wedge y\in 𝒫\bigcup A\right)\to x\cap y\in 𝒫\bigcup A$$
13	12	rgen2	$$⊢\forall x\in 𝒫\bigcup A\forall y\in 𝒫\bigcup Ax\cap y\in 𝒫\bigcup A$$
14		inficl	$$⊢𝒫\bigcup A\in \mathrm{V}\to \left(\forall x\in 𝒫\bigcup A\forall y\in 𝒫\bigcup Ax\cap y\in 𝒫\bigcup A\leftrightarrow \mathrm{fi}\left(𝒫\bigcup A\right)=𝒫\bigcup A\right)$$
15	2 14	syl	$$⊢A\in \mathrm{V}\to \left(\forall x\in 𝒫\bigcup A\forall y\in 𝒫\bigcup Ax\cap y\in 𝒫\bigcup A\leftrightarrow \mathrm{fi}\left(𝒫\bigcup A\right)=𝒫\bigcup A\right)$$
16	13 15	mpbii	$$⊢A\in \mathrm{V}\to \mathrm{fi}\left(𝒫\bigcup A\right)=𝒫\bigcup A$$
17	5 16	sseqtrd	$$⊢A\in \mathrm{V}\to \mathrm{fi}\left(A\right)\subseteq 𝒫\bigcup A$$
18		fvprc	$$⊢\neg A\in \mathrm{V}\to \mathrm{fi}\left(A\right)=\varnothing$$
19		0ss	$$⊢\varnothing \subseteq 𝒫\bigcup A$$
20	18 19	eqsstrdi	$$⊢\neg A\in \mathrm{V}\to \mathrm{fi}\left(A\right)\subseteq 𝒫\bigcup A$$
21	17 20	pm2.61i	$$⊢\mathrm{fi}\left(A\right)\subseteq 𝒫\bigcup A$$