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

Metamath Proof Explorer

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