Metamath Proof Explorer

Theorem ismntop

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

Ref Expression
Assertion ismntop ( ( 𝑁 ∈ ℕ0 ∧ 𝐽 ∈ 𝑉 ) → ( 𝑁 ManTop 𝐽 ↔ ( 𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ismntoplly ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐽 ∈ 𝑉 ) → ( 𝑁 ManTop 𝐽 ↔ ( 𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) ) )
2 haustop ⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Top )
3 2 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐽 ∈ Haus ) → 𝐽 ∈ Top )
4 3 biantrurd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐽 ∈ Haus ) → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) ) ) )
5 hmpher ⊢ ≃ Er Top
6 errel ⊢ ( ≃ Er Top → Rel ≃ )
7 relelec ⊢ ( Rel ≃ → ( ( 𝐽 ↾t 𝑢 ) ∈ [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ↔ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ≃ ( 𝐽 ↾t 𝑢 ) ) )
8 5 6 7 mp2b ⊢ ( ( 𝐽 ↾t 𝑢 ) ∈ [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ↔ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ≃ ( 𝐽 ↾t 𝑢 ) )
9 hmphsymb ⊢ ( ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ≃ ( 𝐽 ↾t 𝑢 ) ↔ ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) )
10 8 9 bitr2i ⊢ ( ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ↔ ( 𝐽 ↾t 𝑢 ) ∈ [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ )
11 10 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐽 ∈ Haus ) → ( ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ↔ ( 𝐽 ↾t 𝑢 ) ∈ [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) )
12 11 anbi2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐽 ∈ Haus ) → ( ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ) ↔ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) ) )
13 12 rexbidv ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐽 ∈ Haus ) → ( ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ) ↔ ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) ) )
14 13 2ralbidv ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐽 ∈ Haus ) → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ) ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) ) )
15 islly ⊢ ( 𝐽 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) ) )
16 15 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐽 ∈ Haus ) → ( 𝐽 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) ) ) )
17 4 14 16 3bitr4rd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐽 ∈ Haus ) → ( 𝐽 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ) ) )
18 17 pm5.32da ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) ↔ ( 𝐽 ∈ Haus ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ) ) ) )
19 18 anbi2d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝐽 ∈ 2ndω ∧ ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) ) ↔ ( 𝐽 ∈ 2ndω ∧ ( 𝐽 ∈ Haus ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ) ) ) ) )
20 3anass ⊢ ( ( 𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) ↔ ( 𝐽 ∈ 2ndω ∧ ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) ) )
21 3anass ⊢ ( ( 𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ) ) ↔ ( 𝐽 ∈ 2ndω ∧ ( 𝐽 ∈ Haus ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ) ) ) )
22 19 20 21 3bitr4g ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) ↔ ( 𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ) ) ) )
23 22 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐽 ∈ 𝑉 ) → ( ( 𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ] ≃ ) ↔ ( 𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ) ) ) )
24 1 23 bitrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐽 ∈ 𝑉 ) → ( 𝑁 ManTop 𝐽 ↔ ( 𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ≃ ( TopOpen ‘ ( 𝔼hil ‘ 𝑁 ) ) ) ) ) )