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 → N ManTop J ↔ J ∈ 2 nd 𝜔 ∧ 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 ∈ 2 nd 𝜔 ↔ J ∈ 2 nd 𝜔
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 ∈ 2 nd 𝜔 ∧ j ∈ Haus ∧ j ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ n ≃ ↔ J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ J ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ N ≃
14 3 13 anbi12d ⊢ n = N ∧ j = J → n ∈ ℕ 0 ∧ j ∈ 2 nd 𝜔 ∧ j ∈ Haus ∧ j ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ n ≃ ↔ N ∈ ℕ 0 ∧ J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ J ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ N ≃
15 df-mntop ⊢ ManTop = n j | n ∈ ℕ 0 ∧ j ∈ 2 nd 𝜔 ∧ j ∈ Haus ∧ j ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ n ≃
16 14 15 brabga ⊢ N ∈ ℕ 0 ∧ J ∈ V → N ManTop J ↔ N ∈ ℕ 0 ∧ J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ J ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ N ≃
17 1 16 mpbirand ⊢ N ∈ ℕ 0 ∧ J ∈ V → N ManTop J ↔ J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ J ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ N ≃