Metamath Proof Explorer

Theorem ismntop

Description: Property of being a manifold. (Contributed by Thierry Arnoux, 5-Jan-2020)

Ref Expression
Assertion ismntop ⊢ N ∈ ℕ 0 ∧ J ∈ V → N ManTop J ↔ J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N

Proof

Step Hyp Ref Expression
1 ismntoplly ⊢ N ∈ ℕ 0 ∧ J ∈ V → N ManTop J ↔ J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ J ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ N ≃
2 haustop ⊢ J ∈ Haus → J ∈ Top
3 2 adantl ⊢ N ∈ ℕ 0 ∧ J ∈ Haus → J ∈ Top
4 3 biantrurd ⊢ N ∈ ℕ 0 ∧ J ∈ Haus → ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ∈ TopOpen ⁡ 𝔼 hil ⁡ N ≃ ↔ J ∈ Top ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ∈ TopOpen ⁡ 𝔼 hil ⁡ N ≃
5 hmpher ⊢ ≃ Er Top
6 errel ⊢ ≃ Er Top → Rel ⁡ ≃
7 relelec ⊢ Rel ⁡ ≃ → J ↾ 𝑡 u ∈ TopOpen ⁡ 𝔼 hil ⁡ N ≃ ↔ TopOpen ⁡ 𝔼 hil ⁡ N ≃ J ↾ 𝑡 u
8 5 6 7 mp2b ⊢ J ↾ 𝑡 u ∈ TopOpen ⁡ 𝔼 hil ⁡ N ≃ ↔ TopOpen ⁡ 𝔼 hil ⁡ N ≃ J ↾ 𝑡 u
9 hmphsymb ⊢ TopOpen ⁡ 𝔼 hil ⁡ N ≃ J ↾ 𝑡 u ↔ J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N
10 8 9 bitr2i ⊢ J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N ↔ J ↾ 𝑡 u ∈ TopOpen ⁡ 𝔼 hil ⁡ N ≃
11 10 a1i ⊢ N ∈ ℕ 0 ∧ J ∈ Haus → J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N ↔ J ↾ 𝑡 u ∈ TopOpen ⁡ 𝔼 hil ⁡ N ≃
12 11 anbi2d ⊢ N ∈ ℕ 0 ∧ J ∈ Haus → y ∈ u ∧ J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N ↔ y ∈ u ∧ J ↾ 𝑡 u ∈ TopOpen ⁡ 𝔼 hil ⁡ N ≃
13 12 rexbidv ⊢ N ∈ ℕ 0 ∧ J ∈ Haus → ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N ↔ ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ∈ TopOpen ⁡ 𝔼 hil ⁡ N ≃
14 13 2ralbidv ⊢ N ∈ ℕ 0 ∧ J ∈ Haus → ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N ↔ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ∈ TopOpen ⁡ 𝔼 hil ⁡ N ≃
15 islly ⊢ J ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ N ≃ ↔ J ∈ Top ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ∈ TopOpen ⁡ 𝔼 hil ⁡ N ≃
16 15 a1i ⊢ N ∈ ℕ 0 ∧ J ∈ Haus → J ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ N ≃ ↔ J ∈ Top ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ∈ TopOpen ⁡ 𝔼 hil ⁡ N ≃
17 4 14 16 3bitr4rd ⊢ N ∈ ℕ 0 ∧ J ∈ Haus → J ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ N ≃ ↔ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N
18 17 pm5.32da ⊢ N ∈ ℕ 0 → J ∈ Haus ∧ J ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ N ≃ ↔ J ∈ Haus ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N
19 18 anbi2d ⊢ N ∈ ℕ 0 → J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ J ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ N ≃ ↔ J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N
20 3anass ⊢ J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ J ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ N ≃ ↔ J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ J ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ N ≃
21 3anass ⊢ J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N ↔ J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N
22 19 20 21 3bitr4g ⊢ N ∈ ℕ 0 → J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ J ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ N ≃ ↔ J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N
23 22 adantr ⊢ N ∈ ℕ 0 ∧ J ∈ V → J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ J ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ N ≃ ↔ J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N
24 1 23 bitrd ⊢ N ∈ ℕ 0 ∧ J ∈ V → N ManTop J ↔ J ∈ 2 nd 𝜔 ∧ J ∈ Haus ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ J ∩ 𝒫 x y ∈ u ∧ J ↾ 𝑡 u ≃ TopOpen ⁡ 𝔼 hil ⁡ N