Metamath Proof Explorer

Theorem relmntop

Description: Manifold is a relation. (Contributed by Thierry Arnoux, 28-Dec-2019)

Ref Expression
Assertion relmntop 
|- Rel ManTop

Proof

Step Hyp Ref Expression
1 df-mntop 
 |-  ManTop = { <. n , j >. | ( n e. NN0 /\ ( j e. 2ndc /\ j e. Haus /\ j e. Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= ) ) }
2 1 relopabiv 
 |-  Rel ManTop