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


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