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∈AB∈Clsd⁡J→⋃x∈AB∈Clsd⁡J

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢X=⋃J
2 difin ⊢X∖X∩⋂x∈AX∖B=X∖⋂x∈AX∖B
3 iundif2 ⊢⋃x∈AX∖X∖B=X∖⋂x∈AX∖B
4 2 3 eqtr4i ⊢X∖X∩⋂x∈AX∖B=⋃x∈AX∖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∈AB∈Clsd⁡J→∀x∈AX∖X∖B=B
9 8 3ad2ant3 ⊢J∈Top∧A∈Fin∧∀x∈AB∈Clsd⁡J→∀x∈AX∖X∖B=B
10 iuneq2 ⊢∀x∈AX∖X∖B=B→⋃x∈AX∖X∖B=⋃x∈AB
11 9 10 syl ⊢J∈Top∧A∈Fin∧∀x∈AB∈Clsd⁡J→⋃x∈AX∖X∖B=⋃x∈AB
12 4 11 eqtrid ⊢J∈Top∧A∈Fin∧∀x∈AB∈Clsd⁡J→X∖X∩⋂x∈AX∖B=⋃x∈AB
13 simp1 ⊢J∈Top∧A∈Fin∧∀x∈AB∈Clsd⁡J→J∈Top
14 1 cldopn ⊢B∈Clsd⁡J→X∖B∈J
15 14 ralimi ⊢∀x∈AB∈Clsd⁡J→∀x∈AX∖B∈J
16 1 riinopn ⊢J∈Top∧A∈Fin∧∀x∈AX∖B∈J→X∩⋂x∈AX∖B∈J
17 15 16 syl3an3 ⊢J∈Top∧A∈Fin∧∀x∈AB∈Clsd⁡J→X∩⋂x∈AX∖B∈J
18 1 opncld ⊢J∈Top∧X∩⋂x∈AX∖B∈J→X∖X∩⋂x∈AX∖B∈Clsd⁡J
19 13 17 18 syl2anc ⊢J∈Top∧A∈Fin∧∀x∈AB∈Clsd⁡J→X∖X∩⋂x∈AX∖B∈Clsd⁡J
20 12 19 eqeltrrd ⊢J∈Top∧A∈Fin∧∀x∈AB∈Clsd⁡J→⋃x∈AB∈Clsd⁡J