Database
BASIC TOPOLOGY
Topology
Closure and interior
unicld
Next ⟩
clscld
Metamath Proof Explorer
Ascii
Unicode
Theorem
unicld
Description:
A finite union of closed sets is closed.
(Contributed by
Mario Carneiro
, 19-Sep-2015)
Ref
Expression
Hypothesis
clscld.1
⊢
X
=
⋃
J
Assertion
unicld
⊢
J
∈
Top
∧
A
∈
Fin
∧
A
⊆
Clsd
⁡
J
→
⋃
A
∈
Clsd
⁡
J
Proof
Step
Hyp
Ref
Expression
1
clscld.1
⊢
X
=
⋃
J
2
uniiun
⊢
⋃
A
=
⋃
x
∈
A
x
3
dfss3
⊢
A
⊆
Clsd
⁡
J
↔
∀
x
∈
A
x
∈
Clsd
⁡
J
4
1
iuncld
⊢
J
∈
Top
∧
A
∈
Fin
∧
∀
x
∈
A
x
∈
Clsd
⁡
J
→
⋃
x
∈
A
x
∈
Clsd
⁡
J
5
3
4
syl3an3b
⊢
J
∈
Top
∧
A
∈
Fin
∧
A
⊆
Clsd
⁡
J
→
⋃
x
∈
A
x
∈
Clsd
⁡
J
6
2
5
eqeltrid
⊢
J
∈
Top
∧
A
∈
Fin
∧
A
⊆
Clsd
⁡
J
→
⋃
A
∈
Clsd
⁡
J