Metamath Proof Explorer

Theorem iuncld

Description: A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypothesis clscld.1 ⊢ X = ⋃ J
Assertion iuncld ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ Clsd ⁡ J → ⋃ x ∈ A B ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ X = ⋃ J
2 difin ⊢ X ∖ X ∩ ⋂ x ∈ A X ∖ B = X ∖ ⋂ x ∈ A X ∖ B
3 iundif2 ⊢ ⋃ x ∈ A X ∖ X ∖ B = X ∖ ⋂ x ∈ A X ∖ B
4 2 3 eqtr4i ⊢ X ∖ X ∩ ⋂ x ∈ A X ∖ B = ⋃ x ∈ A X ∖ X ∖ B
5 1 cldss ⊢ B ∈ Clsd ⁡ J → B ⊆ X
6 dfss4 ⊢ B ⊆ X ↔ X ∖ X ∖ B = B
7 5 6 sylib ⊢ B ∈ Clsd ⁡ J → X ∖ X ∖ B = B
8 7 ralimi ⊢ ∀ x ∈ A B ∈ Clsd ⁡ J → ∀ x ∈ A X ∖ X ∖ B = B
9 8 3ad2ant3 ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ Clsd ⁡ J → ∀ x ∈ A X ∖ X ∖ B = B
10 iuneq2 ⊢ ∀ x ∈ A X ∖ X ∖ B = B → ⋃ x ∈ A X ∖ X ∖ B = ⋃ x ∈ A B
11 9 10 syl ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ Clsd ⁡ J → ⋃ x ∈ A X ∖ X ∖ B = ⋃ x ∈ A B
12 4 11 syl5eq ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ Clsd ⁡ J → X ∖ X ∩ ⋂ x ∈ A X ∖ B = ⋃ x ∈ A B
13 simp1 ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ Clsd ⁡ J → J ∈ Top
14 1 cldopn ⊢ B ∈ Clsd ⁡ J → X ∖ B ∈ J
15 14 ralimi ⊢ ∀ x ∈ A B ∈ Clsd ⁡ J → ∀ x ∈ A X ∖ B ∈ J
16 1 riinopn ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A X ∖ B ∈ J → X ∩ ⋂ x ∈ A X ∖ B ∈ J
17 15 16 syl3an3 ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ Clsd ⁡ J → X ∩ ⋂ x ∈ A X ∖ B ∈ J
18 1 opncld ⊢ J ∈ Top ∧ X ∩ ⋂ x ∈ A X ∖ B ∈ J → X ∖ X ∩ ⋂ x ∈ A X ∖ B ∈ Clsd ⁡ J
19 13 17 18 syl2anc ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ Clsd ⁡ J → X ∖ X ∩ ⋂ x ∈ A X ∖ B ∈ Clsd ⁡ J
20 12 19 eqeltrrd ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ Clsd ⁡ J → ⋃ x ∈ A B ∈ Clsd ⁡ J