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