Theorem iundifdifd

Description: The intersection of a set is the complement of the union of the complements. (Contributed by Thierry Arnoux, 19-Dec-2016)

	Ref	Expression
Assertion	iundifdifd	$$⊢A\subseteq 𝒫O\to \left(A\ne \varnothing \to \bigcap A=O\setminus \bigcup _{x\in A}\left(O\setminus x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		iundif2	$$⊢\bigcup _{x\in A}\left(O\setminus x\right)=O\setminus \bigcap _{x\in A}x$$
2		intiin	$$⊢\bigcap A=\bigcap _{x\in A}x$$
3	2	difeq2i	$$⊢O\setminus \bigcap A=O\setminus \bigcap _{x\in A}x$$
4	1 3	eqtr4i	$$⊢\bigcup _{x\in A}\left(O\setminus x\right)=O\setminus \bigcap A$$
5	4	difeq2i	$$⊢O\setminus \bigcup _{x\in A}\left(O\setminus x\right)=O\setminus \left(O\setminus \bigcap A\right)$$
6		intssuni2	$$⊢\left(A\subseteq 𝒫O\wedge A\ne \varnothing \right)\to \bigcap A\subseteq \bigcup 𝒫O$$
7		unipw	$$⊢\bigcup 𝒫O=O$$
8	6 7	sseqtrdi	$$⊢\left(A\subseteq 𝒫O\wedge A\ne \varnothing \right)\to \bigcap A\subseteq O$$
9		dfss4	$$⊢\bigcap A\subseteq O\leftrightarrow O\setminus \left(O\setminus \bigcap A\right)=\bigcap A$$
10	8 9	sylib	$$⊢\left(A\subseteq 𝒫O\wedge A\ne \varnothing \right)\to O\setminus \left(O\setminus \bigcap A\right)=\bigcap A$$
11	5 10	eqtr2id	$$⊢\left(A\subseteq 𝒫O\wedge A\ne \varnothing \right)\to \bigcap A=O\setminus \bigcup _{x\in A}\left(O\setminus x\right)$$
12	11	ex	$$⊢A\subseteq 𝒫O\to \left(A\ne \varnothing \to \bigcap A=O\setminus \bigcup _{x\in A}\left(O\setminus x\right)\right)$$