Metamath Proof Explorer

Theorem cldrcl

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

Ref Expression
Assertion cldrcl ⊢ C ∈ Clsd ⁡ J → J ∈ Top

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ C ∈ Clsd ⁡ J → J ∈ dom ⁡ Clsd
2 fncld ⊢ Clsd Fn Top
3 2 fndmi ⊢ dom ⁡ Clsd = Top
4 1 3 eleqtrdi ⊢ C ∈ Clsd ⁡ J → J ∈ Top