Metamath Proof Explorer

Theorem ismntoplly

Description: Property of being a manifold. (Contributed by Thierry Arnoux, 28-Dec-2019)

Ref Expression
Assertion ismntoplly ⊢N∈ℕ0∧J∈V→NManTopJ↔J∈2nd𝜔∧J∈Haus∧J∈Locally TopOpen⁡𝔼hil⁡N≃

Proof

Step Hyp Ref Expression
1 simpl ⊢N∈ℕ0∧J∈V→N∈ℕ0
2 simpl ⊢n=N∧j=J→n=N
3 2 eleq1d ⊢n=N∧j=J→n∈ℕ0↔N∈ℕ0
4 simpr ⊢n=N∧j=J→j=J
5 4 eleq1d ⊢n=N∧j=J→j∈2nd𝜔↔J∈2nd𝜔
6 4 eleq1d ⊢n=N∧j=J→j∈Haus↔J∈Haus
7 2fveq3 ⊢n=N→TopOpen⁡𝔼hil⁡n=TopOpen⁡𝔼hil⁡N
8 7 eceq1d ⊢n=N→TopOpen⁡𝔼hil⁡n≃=TopOpen⁡𝔼hil⁡N≃
9 llyeq ⊢TopOpen⁡𝔼hil⁡n≃=TopOpen⁡𝔼hil⁡N≃→Locally TopOpen⁡𝔼hil⁡n≃ = Locally TopOpen⁡𝔼hil⁡N≃
10 8 9 syl ⊢n=N→Locally TopOpen⁡𝔼hil⁡n≃ = Locally TopOpen⁡𝔼hil⁡N≃
11 10 adantr ⊢n=N∧j=J→Locally TopOpen⁡𝔼hil⁡n≃ = Locally TopOpen⁡𝔼hil⁡N≃
12 4 11 eleq12d ⊢n=N∧j=J→j∈Locally TopOpen⁡𝔼hil⁡n≃ ↔ J∈Locally TopOpen⁡𝔼hil⁡N≃
13 5 6 12 3anbi123d ⊢n=N∧j=J→j∈2nd𝜔∧j∈Haus∧j∈Locally TopOpen⁡𝔼hil⁡n≃ ↔ J∈2nd𝜔∧J∈Haus∧J∈Locally TopOpen⁡𝔼hil⁡N≃
14 3 13 anbi12d ⊢n=N∧j=J→n∈ℕ0∧j∈2nd𝜔∧j∈Haus∧j∈Locally TopOpen⁡𝔼hil⁡n≃ ↔ N∈ℕ0∧J∈2nd𝜔∧J∈Haus∧J∈Locally TopOpen⁡𝔼hil⁡N≃
15 df-mntop ⊢ManTop=nj|n∈ℕ0∧j∈2nd𝜔∧j∈Haus∧j∈Locally TopOpen⁡𝔼hil⁡n≃
16 14 15 brabga ⊢N∈ℕ0∧J∈V→NManTopJ↔N∈ℕ0∧J∈2nd𝜔∧J∈Haus∧J∈Locally TopOpen⁡𝔼hil⁡N≃
17 1 16 mpbirand ⊢N∈ℕ0∧J∈V→NManTopJ↔J∈2nd𝜔∧J∈Haus∧J∈Locally TopOpen⁡𝔼hil⁡N≃