Theorem cldrcl

Description: Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Assertion	cldrcl	⊢ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ dom Clsd )
2		fncld	⊢ Clsd Fn Top
3	2	fndmi	⊢ dom Clsd = Top
4	1 3	eleqtrdi	⊢ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Top )