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 = { ⟨ 𝑛 , 𝑗 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ ( 𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃ ) ) }
2	1	relopabiv	⊢ Rel ManTop