Theorem clsss

Description: Subset relationship for closure. (Contributed by NM, 10-Feb-2007)

	Ref	Expression
Hypothesis	clscld.1	⊢ 𝑋 = ∪ 𝐽
Assertion	clsss	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	⊢ 𝑋 = ∪ 𝐽
2		sstr2	⊢ ( 𝑇 ⊆ 𝑆 → ( 𝑆 ⊆ 𝑥 → 𝑇 ⊆ 𝑥 ) )
3	2	adantr	⊢ ( ( 𝑇 ⊆ 𝑆 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑆 ⊆ 𝑥 → 𝑇 ⊆ 𝑥 ) )
4	3	ss2rabdv	⊢ ( 𝑇 ⊆ 𝑆 → { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } ⊆ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑇 ⊆ 𝑥 } )
5		intss	⊢ ( { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } ⊆ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑇 ⊆ 𝑥 } → ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑇 ⊆ 𝑥 } ⊆ ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )
6	4 5	syl	⊢ ( 𝑇 ⊆ 𝑆 → ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑇 ⊆ 𝑥 } ⊆ ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )
7	6	3ad2ant3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) → ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑇 ⊆ 𝑥 } ⊆ ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )
8		simp1	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) → 𝐽 ∈ Top )
9		sstr2	⊢ ( 𝑇 ⊆ 𝑆 → ( 𝑆 ⊆ 𝑋 → 𝑇 ⊆ 𝑋 ) )
10	9	impcom	⊢ ( ( 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) → 𝑇 ⊆ 𝑋 )
11	10	3adant1	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) → 𝑇 ⊆ 𝑋 )
12	1	clsval	⊢ ( ( 𝐽 ∈ Top ∧ 𝑇 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) = ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑇 ⊆ 𝑥 } )
13	8 11 12	syl2anc	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) = ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑇 ⊆ 𝑥 } )
14	1	clsval	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )
15	14	3adant3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )
16	7 13 15	3sstr4d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )