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

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 ⊢ 𝑋 = ∪ 𝐽
Assertion iuncld ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ 𝑋 = ∪ 𝐽
2 difin ⊢ ( 𝑋 ∖ ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 ( 𝑋 ∖ 𝐵 ) ) ) = ( 𝑋 ∖ ∩ 𝑥 ∈ 𝐴 ( 𝑋 ∖ 𝐵 ) )
3 iundif2 ⊢ ∪ 𝑥 ∈ 𝐴 ( 𝑋 ∖ ( 𝑋 ∖ 𝐵 ) ) = ( 𝑋 ∖ ∩ 𝑥 ∈ 𝐴 ( 𝑋 ∖ 𝐵 ) )
4 2 3 eqtr4i ⊢ ( 𝑋 ∖ ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 ( 𝑋 ∖ 𝐵 ) ) ) = ∪ 𝑥 ∈ 𝐴 ( 𝑋 ∖ ( 𝑋 ∖ 𝐵 ) )
5 1 cldss ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → 𝐵 ⊆ 𝑋 )
6 dfss4 ⊢ ( 𝐵 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝐵 ) ) = 𝐵 )
7 5 6 sylib ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝐵 ) ) = 𝐵 )
8 7 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑋 ∖ ( 𝑋 ∖ 𝐵 ) ) = 𝐵 )
9 8 3ad2ant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑋 ∖ ( 𝑋 ∖ 𝐵 ) ) = 𝐵 )
10 iuneq2 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑋 ∖ ( 𝑋 ∖ 𝐵 ) ) = 𝐵 → ∪ 𝑥 ∈ 𝐴 ( 𝑋 ∖ ( 𝑋 ∖ 𝐵 ) ) = ∪ 𝑥 ∈ 𝐴 𝐵 )
11 9 10 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∪ 𝑥 ∈ 𝐴 ( 𝑋 ∖ ( 𝑋 ∖ 𝐵 ) ) = ∪ 𝑥 ∈ 𝐴 𝐵 )
12 4 11 eqtrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ∖ ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 ( 𝑋 ∖ 𝐵 ) ) ) = ∪ 𝑥 ∈ 𝐴 𝐵 )
13 simp1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐽 ∈ Top )
14 1 cldopn ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑋 ∖ 𝐵 ) ∈ 𝐽 )
15 14 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑋 ∖ 𝐵 ) ∈ 𝐽 )
16 1 riinopn ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑋 ∖ 𝐵 ) ∈ 𝐽 ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 ( 𝑋 ∖ 𝐵 ) ) ∈ 𝐽 )
17 15 16 syl3an3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 ( 𝑋 ∖ 𝐵 ) ) ∈ 𝐽 )
18 1 opncld ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 ( 𝑋 ∖ 𝐵 ) ) ∈ 𝐽 ) → ( 𝑋 ∖ ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 ( 𝑋 ∖ 𝐵 ) ) ) ∈ ( Clsd ‘ 𝐽 ) )
19 13 17 18 syl2anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ∖ ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 ( 𝑋 ∖ 𝐵 ) ) ) ∈ ( Clsd ‘ 𝐽 ) )
20 12 19 eqeltrrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) )