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 ⊢ O ∈ V
iundifdif.2 ⊢ A ⊆ 𝒫 O
Assertion iundifdif ⊢ A ≠ ∅ → ⋂ A = O ∖ ⋃ x ∈ A O ∖ x

Proof

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