Theorem cls0

Description: The closure of the empty set. (Contributed by NM, 2-Oct-2007) (Proof shortened by Jim Kingdon, 12-Mar-2023)

	Ref	Expression
Assertion	cls0	⊢ ( 𝐽 ∈ Top → ( ( cls ‘ 𝐽 ) ‘ ∅ ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		0cld	⊢ ( 𝐽 ∈ Top → ∅ ∈ ( Clsd ‘ 𝐽 ) )
2		cldcls	⊢ ( ∅ ∈ ( Clsd ‘ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ∅ ) = ∅ )
3	1 2	syl	⊢ ( 𝐽 ∈ Top → ( ( cls ‘ 𝐽 ) ‘ ∅ ) = ∅ )