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

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 ( ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐴 ∪ 𝐵 ) ∈ ( Clsd ‘ 𝐽 ) )

Proof

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