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 (A \neq \emptyset \to ⋂ A = O ∖ ⋃_{x \in A} (O ∖ x))$

Step	Hyp	Ref	Expression
1		iundif2	$⊢ ⋃_{x \in A} (O ∖ x) = O ∖ ⋂_{x \in A} x$
2		intiin	$⊢ ⋂ A = ⋂_{x \in A} x$
3	2	difeq2i	$⊢ O ∖ ⋂ A = O ∖ ⋂_{x \in A} x$
4	1 3	eqtr4i	$⊢ ⋃_{x \in A} (O ∖ x) = O ∖ ⋂ A$
5	4	difeq2i	$⊢ O ∖ ⋃_{x \in A} (O ∖ x) = O ∖ (O ∖ ⋂ A)$
6		intssuni2	$⊢ (A \subseteq 𝒫 O \land A \neq \emptyset) \to ⋂ A \subseteq ⋃ 𝒫 O$
7		unipw	$⊢ ⋃ 𝒫 O = O$
8	6 7	sseqtrdi	$⊢ (A \subseteq 𝒫 O \land A \neq \emptyset) \to ⋂ A \subseteq O$
9		dfss4	$⊢ ⋂ A \subseteq O \leftrightarrow O ∖ (O ∖ ⋂ A) = ⋂ A$
10	8 9	sylib	$⊢ (A \subseteq 𝒫 O \land A \neq \emptyset) \to O ∖ (O ∖ ⋂ A) = ⋂ A$
11	5 10	eqtr2id	$⊢ (A \subseteq 𝒫 O \land A \neq \emptyset) \to ⋂ A = O ∖ ⋃_{x \in A} (O ∖ x)$
12	11	ex	$⊢ A \subseteq 𝒫 O \to (A \neq \emptyset \to ⋂ A = O ∖ ⋃_{x \in A} (O ∖ x))$

Metamath Proof Explorer