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

Proof

Step	Hyp	Ref	Expression
1		iundifdif.o	⊢ 𝑂 ∈ V
2		iundifdif.2	⊢ 𝐴 ⊆ 𝒫 𝑂
3		iundif2	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝑂 ∖ 𝑥 ) = ( 𝑂 ∖ ∩ 𝑥 ∈ 𝐴 𝑥 )
4		intiin	⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥
5	4	difeq2i	⊢ ( 𝑂 ∖ ∩ 𝐴 ) = ( 𝑂 ∖ ∩ 𝑥 ∈ 𝐴 𝑥 )
6	3 5	eqtr4i	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝑂 ∖ 𝑥 ) = ( 𝑂 ∖ ∩ 𝐴 )
7	6	difeq2i	⊢ ( 𝑂 ∖ ∪ 𝑥 ∈ 𝐴 ( 𝑂 ∖ 𝑥 ) ) = ( 𝑂 ∖ ( 𝑂 ∖ ∩ 𝐴 ) )
8	2	jctl	⊢ ( 𝐴 ≠ ∅ → ( 𝐴 ⊆ 𝒫 𝑂 ∧ 𝐴 ≠ ∅ ) )
9		intssuni2	⊢ ( ( 𝐴 ⊆ 𝒫 𝑂 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ⊆ ∪ 𝒫 𝑂 )
10		unipw	⊢ ∪ 𝒫 𝑂 = 𝑂
11	10	sseq2i	⊢ ( ∩ 𝐴 ⊆ ∪ 𝒫 𝑂 ↔ ∩ 𝐴 ⊆ 𝑂 )
12	11	biimpi	⊢ ( ∩ 𝐴 ⊆ ∪ 𝒫 𝑂 → ∩ 𝐴 ⊆ 𝑂 )
13	8 9 12	3syl	⊢ ( 𝐴 ≠ ∅ → ∩ 𝐴 ⊆ 𝑂 )
14		dfss4	⊢ ( ∩ 𝐴 ⊆ 𝑂 ↔ ( 𝑂 ∖ ( 𝑂 ∖ ∩ 𝐴 ) ) = ∩ 𝐴 )
15	13 14	sylib	⊢ ( 𝐴 ≠ ∅ → ( 𝑂 ∖ ( 𝑂 ∖ ∩ 𝐴 ) ) = ∩ 𝐴 )
16	7 15	eqtr2id	⊢ ( 𝐴 ≠ ∅ → ∩ 𝐴 = ( 𝑂 ∖ ∪ 𝑥 ∈ 𝐴 ( 𝑂 ∖ 𝑥 ) ) )