Metamath Proof Explorer

Theorem cldmreon

Description: The closed sets of a topology over a set are a Moore collection over the same set. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Assertion cldmreon 
|- ( J e. ( TopOn ` B ) -> ( Clsd ` J ) e. ( Moore ` B ) )

Proof

Step Hyp Ref Expression
1 topontop 
 |-  ( J e. ( TopOn ` B ) -> J e. Top )
2 eqid 
 |-  U. J = U. J
3 2 cldmre 
 |-  ( J e. Top -> ( Clsd ` J ) e. ( Moore ` U. J ) )
4 1 3 syl 
 |-  ( J e. ( TopOn ` B ) -> ( Clsd ` J ) e. ( Moore ` U. J ) )
5 toponuni 
 |-  ( J e. ( TopOn ` B ) -> B = U. J )
6 5 fveq2d 
 |-  ( J e. ( TopOn ` B ) -> ( Moore ` B ) = ( Moore ` U. J ) )
7 4 6 eleqtrrd 
 |-  ( J e. ( TopOn ` B ) -> ( Clsd ` J ) e. ( Moore ` B ) )