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

Metamath Proof Explorer

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