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	⊢ ( 𝐴 ⊆ 𝒫 𝑂 → ( 𝐴 ≠ ∅ → ∩ 𝐴 = ( 𝑂 ∖ ∪ 𝑥 ∈ 𝐴 ( 𝑂 ∖ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iundif2	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝑂 ∖ 𝑥 ) = ( 𝑂 ∖ ∩ 𝑥 ∈ 𝐴 𝑥 )
2		intiin	⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥
3	2	difeq2i	⊢ ( 𝑂 ∖ ∩ 𝐴 ) = ( 𝑂 ∖ ∩ 𝑥 ∈ 𝐴 𝑥 )
4	1 3	eqtr4i	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝑂 ∖ 𝑥 ) = ( 𝑂 ∖ ∩ 𝐴 )
5	4	difeq2i	⊢ ( 𝑂 ∖ ∪ 𝑥 ∈ 𝐴 ( 𝑂 ∖ 𝑥 ) ) = ( 𝑂 ∖ ( 𝑂 ∖ ∩ 𝐴 ) )
6		intssuni2	⊢ ( ( 𝐴 ⊆ 𝒫 𝑂 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ⊆ ∪ 𝒫 𝑂 )
7		unipw	⊢ ∪ 𝒫 𝑂 = 𝑂
8	6 7	sseqtrdi	⊢ ( ( 𝐴 ⊆ 𝒫 𝑂 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ⊆ 𝑂 )
9		dfss4	⊢ ( ∩ 𝐴 ⊆ 𝑂 ↔ ( 𝑂 ∖ ( 𝑂 ∖ ∩ 𝐴 ) ) = ∩ 𝐴 )
10	8 9	sylib	⊢ ( ( 𝐴 ⊆ 𝒫 𝑂 ∧ 𝐴 ≠ ∅ ) → ( 𝑂 ∖ ( 𝑂 ∖ ∩ 𝐴 ) ) = ∩ 𝐴 )
11	5 10	eqtr2id	⊢ ( ( 𝐴 ⊆ 𝒫 𝑂 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 = ( 𝑂 ∖ ∪ 𝑥 ∈ 𝐴 ( 𝑂 ∖ 𝑥 ) ) )
12	11	ex	⊢ ( 𝐴 ⊆ 𝒫 𝑂 → ( 𝐴 ≠ ∅ → ∩ 𝐴 = ( 𝑂 ∖ ∪ 𝑥 ∈ 𝐴 ( 𝑂 ∖ 𝑥 ) ) ) )