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 e. ( Clsd ` J ) -> J e. Top )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( C e. ( Clsd ` J ) -> J e. dom Clsd )
2 fncld 
 |-  Clsd Fn Top
3 2 fndmi 
 |-  dom Clsd = Top
4 1 3 eleqtrdi 
 |-  ( C e. ( Clsd ` J ) -> J e. Top )