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 ‘ 𝐽 ) )