Theorem iscld4

Description: A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008)

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

Proof

Step	Hyp	Ref	Expression
1		clscld.1	⊢ 𝑋 = ∪ 𝐽
2	1	iscld3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )
3		eqss	⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ∧ 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
4	1	sscls	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
5	4	biantrud	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ∧ 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
6	3 5	bitr4id	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) )
7	2 6	bitrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) )