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