Theorem iundifdif

Description: The intersection of a set is the complement of the union of the complements. TODO: shorten using iundifdifd . (Contributed by Thierry Arnoux, 4-Sep-2016)

	Ref	Expression
Hypotheses	iundifdif.o	$$⊢O\in \mathrm{V}$$
	iundifdif.2	$$⊢A\subseteq 𝒫O$$
Assertion	iundifdif	$$⊢A\ne \varnothing \to \bigcap A=O\setminus \bigcup _{x\in A}\left(O\setminus x\right)$$

Proof

Step	Hyp	Ref	Expression
1		iundifdif.o	$$⊢O\in \mathrm{V}$$
2		iundifdif.2	$$⊢A\subseteq 𝒫O$$
3		iundif2	$$⊢\bigcup _{x\in A}\left(O\setminus x\right)=O\setminus \bigcap _{x\in A}x$$
4		intiin	$$⊢\bigcap A=\bigcap _{x\in A}x$$
5	4	difeq2i	$$⊢O\setminus \bigcap A=O\setminus \bigcap _{x\in A}x$$
6	3 5	eqtr4i	$$⊢\bigcup _{x\in A}\left(O\setminus x\right)=O\setminus \bigcap A$$
7	6	difeq2i	$$⊢O\setminus \bigcup _{x\in A}\left(O\setminus x\right)=O\setminus \left(O\setminus \bigcap A\right)$$
8	2	jctl	$$⊢A\ne \varnothing \to \left(A\subseteq 𝒫O\wedge A\ne \varnothing \right)$$
9		intssuni2	$$⊢\left(A\subseteq 𝒫O\wedge A\ne \varnothing \right)\to \bigcap A\subseteq \bigcup 𝒫O$$
10		unipw	$$⊢\bigcup 𝒫O=O$$
11	10	sseq2i	$$⊢\bigcap A\subseteq \bigcup 𝒫O\leftrightarrow \bigcap A\subseteq O$$
12	11	biimpi	$$⊢\bigcap A\subseteq \bigcup 𝒫O\to \bigcap A\subseteq O$$
13	8 9 12	3syl	$$⊢A\ne \varnothing \to \bigcap A\subseteq O$$
14		dfss4	$$⊢\bigcap A\subseteq O\leftrightarrow O\setminus \left(O\setminus \bigcap A\right)=\bigcap A$$
15	13 14	sylib	$$⊢A\ne \varnothing \to O\setminus \left(O\setminus \bigcap A\right)=\bigcap A$$
16	7 15	eqtr2id	$$⊢A\ne \varnothing \to \bigcap A=O\setminus \bigcup _{x\in A}\left(O\setminus x\right)$$