Metamath Proof Explorer

Theorem relmntop

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

		Ref	Expression
	Assertion	relmntop	$⊢ Rel ManTop$

Step	Hyp	Ref	Expression
1		df-mntop	$⊢ ManTop = \{⟨n, j⟩ \| (n \in ℕ_{0} \land (j \in 2^{nd} 𝜔 \land j \in Haus \land j \in Locally[TopOpen (𝔼_{hil} (n))] ≃))\}$
2	1	relopabiv	$⊢ Rel ManTop$