Metamath Proof Explorer

Theorem uncld

Description: The union of two closed sets is closed. Equivalent to Theorem 6.1(3) of Munkres p. 93. (Contributed by NM, 5-Oct-2006)

Ref Expression
Assertion uncld ⊢ A ∈ Clsd ⁡ J ∧ B ∈ Clsd ⁡ J → A ∪ B ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 difundi ⊢ ⋃ J ∖ A ∪ B = ⋃ J ∖ A ∩ ⋃ J ∖ B
2 cldrcl ⊢ A ∈ Clsd ⁡ J → J ∈ Top
3 eqid ⊢ ⋃ J = ⋃ J
4 3 cldopn ⊢ A ∈ Clsd ⁡ J → ⋃ J ∖ A ∈ J
5 3 cldopn ⊢ B ∈ Clsd ⁡ J → ⋃ J ∖ B ∈ J
6 inopn ⊢ J ∈ Top ∧ ⋃ J ∖ A ∈ J ∧ ⋃ J ∖ B ∈ J → ⋃ J ∖ A ∩ ⋃ J ∖ B ∈ J
7 2 4 5 6 syl2an3an ⊢ A ∈ Clsd ⁡ J ∧ B ∈ Clsd ⁡ J → ⋃ J ∖ A ∩ ⋃ J ∖ B ∈ J
8 1 7 eqeltrid ⊢ A ∈ Clsd ⁡ J ∧ B ∈ Clsd ⁡ J → ⋃ J ∖ A ∪ B ∈ J
9 3 cldss ⊢ A ∈ Clsd ⁡ J → A ⊆ ⋃ J
10 3 cldss ⊢ B ∈ Clsd ⁡ J → B ⊆ ⋃ J
11 9 10 anim12i ⊢ A ∈ Clsd ⁡ J ∧ B ∈ Clsd ⁡ J → A ⊆ ⋃ J ∧ B ⊆ ⋃ J
12 unss ⊢ A ⊆ ⋃ J ∧ B ⊆ ⋃ J ↔ A ∪ B ⊆ ⋃ J
13 11 12 sylib ⊢ A ∈ Clsd ⁡ J ∧ B ∈ Clsd ⁡ J → A ∪ B ⊆ ⋃ J
14 3 iscld2 ⊢ J ∈ Top ∧ A ∪ B ⊆ ⋃ J → A ∪ B ∈ Clsd ⁡ J ↔ ⋃ J ∖ A ∪ B ∈ J
15 2 13 14 syl2an2r ⊢ A ∈ Clsd ⁡ J ∧ B ∈ Clsd ⁡ J → A ∪ B ∈ Clsd ⁡ J ↔ ⋃ J ∖ A ∪ B ∈ J
16 8 15 mpbird ⊢ A ∈ Clsd ⁡ J ∧ B ∈ Clsd ⁡ J → A ∪ B ∈ Clsd ⁡ J