This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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