Metamath Proof Explorer

Theorem clsun

Description: A pairwise union of closures is the closure of the union. (Contributed by Jeff Hankins, 31-Aug-2009)

Ref Expression
Hypothesis clsun.1 ⊢ X = ⋃ J
Assertion clsun ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → cls ⁡ J ⁡ A ∪ B = cls ⁡ J ⁡ A ∪ cls ⁡ J ⁡ B

Proof

Step Hyp Ref Expression
1 clsun.1 ⊢ X = ⋃ J
2 difundi ⊢ X ∖ A ∪ B = X ∖ A ∩ X ∖ B
3 2 fveq2i ⊢ int ⁡ J ⁡ X ∖ A ∪ B = int ⁡ J ⁡ X ∖ A ∩ X ∖ B
4 difss ⊢ X ∖ A ⊆ X
5 difss ⊢ X ∖ B ⊆ X
6 1 ntrin ⊢ J ∈ Top ∧ X ∖ A ⊆ X ∧ X ∖ B ⊆ X → int ⁡ J ⁡ X ∖ A ∩ X ∖ B = int ⁡ J ⁡ X ∖ A ∩ int ⁡ J ⁡ X ∖ B
7 4 5 6 mp3an23 ⊢ J ∈ Top → int ⁡ J ⁡ X ∖ A ∩ X ∖ B = int ⁡ J ⁡ X ∖ A ∩ int ⁡ J ⁡ X ∖ B
8 7 3ad2ant1 ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → int ⁡ J ⁡ X ∖ A ∩ X ∖ B = int ⁡ J ⁡ X ∖ A ∩ int ⁡ J ⁡ X ∖ B
9 3 8 syl5eq ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → int ⁡ J ⁡ X ∖ A ∪ B = int ⁡ J ⁡ X ∖ A ∩ int ⁡ J ⁡ X ∖ B
10 simp1 ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → J ∈ Top
11 unss ⊢ A ⊆ X ∧ B ⊆ X ↔ A ∪ B ⊆ X
12 11 biimpi ⊢ A ⊆ X ∧ B ⊆ X → A ∪ B ⊆ X
13 12 3adant1 ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → A ∪ B ⊆ X
14 1 ntrdif ⊢ J ∈ Top ∧ A ∪ B ⊆ X → int ⁡ J ⁡ X ∖ A ∪ B = X ∖ cls ⁡ J ⁡ A ∪ B
15 10 13 14 syl2anc ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → int ⁡ J ⁡ X ∖ A ∪ B = X ∖ cls ⁡ J ⁡ A ∪ B
16 1 ntrdif ⊢ J ∈ Top ∧ A ⊆ X → int ⁡ J ⁡ X ∖ A = X ∖ cls ⁡ J ⁡ A
17 16 3adant3 ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → int ⁡ J ⁡ X ∖ A = X ∖ cls ⁡ J ⁡ A
18 1 ntrdif ⊢ J ∈ Top ∧ B ⊆ X → int ⁡ J ⁡ X ∖ B = X ∖ cls ⁡ J ⁡ B
19 18 3adant2 ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → int ⁡ J ⁡ X ∖ B = X ∖ cls ⁡ J ⁡ B
20 17 19 ineq12d ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → int ⁡ J ⁡ X ∖ A ∩ int ⁡ J ⁡ X ∖ B = X ∖ cls ⁡ J ⁡ A ∩ X ∖ cls ⁡ J ⁡ B
21 difundi ⊢ X ∖ cls ⁡ J ⁡ A ∪ cls ⁡ J ⁡ B = X ∖ cls ⁡ J ⁡ A ∩ X ∖ cls ⁡ J ⁡ B
22 20 21 eqtr4di ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → int ⁡ J ⁡ X ∖ A ∩ int ⁡ J ⁡ X ∖ B = X ∖ cls ⁡ J ⁡ A ∪ cls ⁡ J ⁡ B
23 9 15 22 3eqtr3d ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → X ∖ cls ⁡ J ⁡ A ∪ B = X ∖ cls ⁡ J ⁡ A ∪ cls ⁡ J ⁡ B
24 23 difeq2d ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → X ∖ X ∖ cls ⁡ J ⁡ A ∪ B = X ∖ X ∖ cls ⁡ J ⁡ A ∪ cls ⁡ J ⁡ B
25 1 clscld ⊢ J ∈ Top ∧ A ∪ B ⊆ X → cls ⁡ J ⁡ A ∪ B ∈ Clsd ⁡ J
26 10 13 25 syl2anc ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → cls ⁡ J ⁡ A ∪ B ∈ Clsd ⁡ J
27 1 cldss ⊢ cls ⁡ J ⁡ A ∪ B ∈ Clsd ⁡ J → cls ⁡ J ⁡ A ∪ B ⊆ X
28 26 27 syl ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → cls ⁡ J ⁡ A ∪ B ⊆ X
29 dfss4 ⊢ cls ⁡ J ⁡ A ∪ B ⊆ X ↔ X ∖ X ∖ cls ⁡ J ⁡ A ∪ B = cls ⁡ J ⁡ A ∪ B
30 28 29 sylib ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → X ∖ X ∖ cls ⁡ J ⁡ A ∪ B = cls ⁡ J ⁡ A ∪ B
31 1 clsss3 ⊢ J ∈ Top ∧ A ⊆ X → cls ⁡ J ⁡ A ⊆ X
32 31 3adant3 ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → cls ⁡ J ⁡ A ⊆ X
33 1 clsss3 ⊢ J ∈ Top ∧ B ⊆ X → cls ⁡ J ⁡ B ⊆ X
34 33 3adant2 ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → cls ⁡ J ⁡ B ⊆ X
35 32 34 jca ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → cls ⁡ J ⁡ A ⊆ X ∧ cls ⁡ J ⁡ B ⊆ X
36 unss ⊢ cls ⁡ J ⁡ A ⊆ X ∧ cls ⁡ J ⁡ B ⊆ X ↔ cls ⁡ J ⁡ A ∪ cls ⁡ J ⁡ B ⊆ X
37 dfss4 ⊢ cls ⁡ J ⁡ A ∪ cls ⁡ J ⁡ B ⊆ X ↔ X ∖ X ∖ cls ⁡ J ⁡ A ∪ cls ⁡ J ⁡ B = cls ⁡ J ⁡ A ∪ cls ⁡ J ⁡ B
38 36 37 bitri ⊢ cls ⁡ J ⁡ A ⊆ X ∧ cls ⁡ J ⁡ B ⊆ X ↔ X ∖ X ∖ cls ⁡ J ⁡ A ∪ cls ⁡ J ⁡ B = cls ⁡ J ⁡ A ∪ cls ⁡ J ⁡ B
39 35 38 sylib ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → X ∖ X ∖ cls ⁡ J ⁡ A ∪ cls ⁡ J ⁡ B = cls ⁡ J ⁡ A ∪ cls ⁡ J ⁡ B
40 24 30 39 3eqtr3d ⊢ J ∈ Top ∧ A ⊆ X ∧ B ⊆ X → cls ⁡ J ⁡ A ∪ B = cls ⁡ J ⁡ A ∪ cls ⁡ J ⁡ B