Theorem cldrcl

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

	Ref	Expression
Assertion	cldrcl	$$⊢C\in \mathrm{Clsd}\left(J\right)\to J\in \mathrm{Top}$$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$$⊢C\in \mathrm{Clsd}\left(J\right)\to J\in \mathrm{dom}\mathrm{Clsd}$$
2		fncld	$$⊢\mathrm{Clsd}Fn\mathrm{Top}$$
3		fndm	$$⊢\mathrm{Clsd}Fn\mathrm{Top}\to \mathrm{dom}\mathrm{Clsd}=\mathrm{Top}$$
4	2 3	ax-mp	$$⊢\mathrm{dom}\mathrm{Clsd}=\mathrm{Top}$$
5	1 4	eleqtrdi	$$⊢C\in \mathrm{Clsd}\left(J\right)\to J\in \mathrm{Top}$$