Theorem clsint2

Description: The closure of an intersection is a subset of the intersection of the closures. (Contributed by Jeff Hankins, 31-Aug-2009)

	Ref	Expression
Hypothesis	clsint2.1	⊢ 𝑋 = ∪ 𝐽
Assertion	clsint2	⊢ ( ( 𝐽 ∈ Top ∧ 𝐶 ⊆ 𝒫 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ∩ 𝐶 ) ⊆ ∩ 𝑐 ∈ 𝐶 ( ( cls ‘ 𝐽 ) ‘ 𝑐 ) )

Proof

Step	Hyp	Ref	Expression
1		clsint2.1	⊢ 𝑋 = ∪ 𝐽
2		sspwuni	⊢ ( 𝐶 ⊆ 𝒫 𝑋 ↔ ∪ 𝐶 ⊆ 𝑋 )
3		elssuni	⊢ ( 𝑐 ∈ 𝐶 → 𝑐 ⊆ ∪ 𝐶 )
4		sstr2	⊢ ( 𝑐 ⊆ ∪ 𝐶 → ( ∪ 𝐶 ⊆ 𝑋 → 𝑐 ⊆ 𝑋 ) )
5	3 4	syl	⊢ ( 𝑐 ∈ 𝐶 → ( ∪ 𝐶 ⊆ 𝑋 → 𝑐 ⊆ 𝑋 ) )
6	5	adantl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑐 ∈ 𝐶 ) → ( ∪ 𝐶 ⊆ 𝑋 → 𝑐 ⊆ 𝑋 ) )
7		intss1	⊢ ( 𝑐 ∈ 𝐶 → ∩ 𝐶 ⊆ 𝑐 )
8	1	clsss	⊢ ( ( 𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋 ∧ ∩ 𝐶 ⊆ 𝑐 ) → ( ( cls ‘ 𝐽 ) ‘ ∩ 𝐶 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑐 ) )
9	7 8	syl3an3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋 ∧ 𝑐 ∈ 𝐶 ) → ( ( cls ‘ 𝐽 ) ‘ ∩ 𝐶 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑐 ) )
10	9	3com23	⊢ ( ( 𝐽 ∈ Top ∧ 𝑐 ∈ 𝐶 ∧ 𝑐 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ∩ 𝐶 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑐 ) )
11	10	3expia	⊢ ( ( 𝐽 ∈ Top ∧ 𝑐 ∈ 𝐶 ) → ( 𝑐 ⊆ 𝑋 → ( ( cls ‘ 𝐽 ) ‘ ∩ 𝐶 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑐 ) ) )
12	6 11	syld	⊢ ( ( 𝐽 ∈ Top ∧ 𝑐 ∈ 𝐶 ) → ( ∪ 𝐶 ⊆ 𝑋 → ( ( cls ‘ 𝐽 ) ‘ ∩ 𝐶 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑐 ) ) )
13	12	impancom	⊢ ( ( 𝐽 ∈ Top ∧ ∪ 𝐶 ⊆ 𝑋 ) → ( 𝑐 ∈ 𝐶 → ( ( cls ‘ 𝐽 ) ‘ ∩ 𝐶 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑐 ) ) )
14	2 13	sylan2b	⊢ ( ( 𝐽 ∈ Top ∧ 𝐶 ⊆ 𝒫 𝑋 ) → ( 𝑐 ∈ 𝐶 → ( ( cls ‘ 𝐽 ) ‘ ∩ 𝐶 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑐 ) ) )
15	14	ralrimiv	⊢ ( ( 𝐽 ∈ Top ∧ 𝐶 ⊆ 𝒫 𝑋 ) → ∀ 𝑐 ∈ 𝐶 ( ( cls ‘ 𝐽 ) ‘ ∩ 𝐶 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑐 ) )
16		ssiin	⊢ ( ( ( cls ‘ 𝐽 ) ‘ ∩ 𝐶 ) ⊆ ∩ 𝑐 ∈ 𝐶 ( ( cls ‘ 𝐽 ) ‘ 𝑐 ) ↔ ∀ 𝑐 ∈ 𝐶 ( ( cls ‘ 𝐽 ) ‘ ∩ 𝐶 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑐 ) )
17	15 16	sylibr	⊢ ( ( 𝐽 ∈ Top ∧ 𝐶 ⊆ 𝒫 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ∩ 𝐶 ) ⊆ ∩ 𝑐 ∈ 𝐶 ( ( cls ‘ 𝐽 ) ‘ 𝑐 ) )