Proof of Theorem ismntop
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ismntoplly 34026 | . 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ 𝑉) → (𝑁ManTop𝐽 ↔ (𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ))) | 
| 2 |  | haustop 23339 | . . . . . . . . 9
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) | 
| 3 | 2 | adantl 481 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ Haus) →
𝐽 ∈
Top) | 
| 4 | 3 | biantrurd 532 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ Haus) →
(∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ) ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈
[(TopOpen‘(𝔼hil‘𝑁))] ≃ )))) | 
| 5 |  | hmpher 23792 | . . . . . . . . . . . . 13
⊢  ≃
Er Top | 
| 6 |  | errel 8754 | . . . . . . . . . . . . 13
⊢ ( ≃
Er Top → Rel ≃ ) | 
| 7 |  | relelec 8792 | . . . . . . . . . . . . 13
⊢ (Rel
≃ → ((𝐽
↾t 𝑢)
∈ [(TopOpen‘(𝔼hil‘𝑁))] ≃ ↔
(TopOpen‘(𝔼hil‘𝑁)) ≃ (𝐽 ↾t 𝑢))) | 
| 8 | 5, 6, 7 | mp2b 10 | . . . . . . . . . . . 12
⊢ ((𝐽 ↾t 𝑢) ∈
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ↔
(TopOpen‘(𝔼hil‘𝑁)) ≃ (𝐽 ↾t 𝑢)) | 
| 9 |  | hmphsymb 23794 | . . . . . . . . . . . 12
⊢
((TopOpen‘(𝔼hil‘𝑁)) ≃ (𝐽 ↾t 𝑢) ↔ (𝐽 ↾t 𝑢) ≃
(TopOpen‘(𝔼hil‘𝑁))) | 
| 10 | 8, 9 | bitr2i 276 | . . . . . . . . . . 11
⊢ ((𝐽 ↾t 𝑢) ≃
(TopOpen‘(𝔼hil‘𝑁)) ↔ (𝐽 ↾t 𝑢) ∈
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ) | 
| 11 | 10 | a1i 11 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ Haus) →
((𝐽 ↾t
𝑢) ≃
(TopOpen‘(𝔼hil‘𝑁)) ↔ (𝐽 ↾t 𝑢) ∈
[(TopOpen‘(𝔼hil‘𝑁))] ≃ )) | 
| 12 | 11 | anbi2d 630 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ Haus) →
((𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃
(TopOpen‘(𝔼hil‘𝑁))) ↔ (𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ))) | 
| 13 | 12 | rexbidv 3179 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ Haus) →
(∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃
(TopOpen‘(𝔼hil‘𝑁))) ↔ ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ))) | 
| 14 | 13 | 2ralbidv 3221 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ Haus) →
(∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃
(TopOpen‘(𝔼hil‘𝑁))) ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ))) | 
| 15 |  | islly 23476 | . . . . . . . 8
⊢ (𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ))) | 
| 16 | 15 | a1i 11 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ Haus) →
(𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈
[(TopOpen‘(𝔼hil‘𝑁))] ≃ )))) | 
| 17 | 4, 14, 16 | 3bitr4rd 312 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ Haus) →
(𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃
(TopOpen‘(𝔼hil‘𝑁))))) | 
| 18 | 17 | pm5.32da 579 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ ((𝐽 ∈ Haus
∧ 𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ) ↔ (𝐽 ∈ Haus ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃
(TopOpen‘(𝔼hil‘𝑁)))))) | 
| 19 | 18 | anbi2d 630 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ ((𝐽 ∈
2ndω ∧ (𝐽 ∈ Haus ∧ 𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ )) ↔ (𝐽 ∈ 2ndω ∧ (𝐽 ∈ Haus ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃
(TopOpen‘(𝔼hil‘𝑁))))))) | 
| 20 |  | 3anass 1095 | . . . 4
⊢ ((𝐽 ∈ 2ndω
∧ 𝐽 ∈ Haus ∧
𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ) ↔ (𝐽 ∈ 2ndω ∧ (𝐽 ∈ Haus ∧ 𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ))) | 
| 21 |  | 3anass 1095 | . . . 4
⊢ ((𝐽 ∈ 2ndω
∧ 𝐽 ∈ Haus ∧
∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃
(TopOpen‘(𝔼hil‘𝑁)))) ↔ (𝐽 ∈ 2ndω ∧ (𝐽 ∈ Haus ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃
(TopOpen‘(𝔼hil‘𝑁)))))) | 
| 22 | 19, 20, 21 | 3bitr4g 314 | . . 3
⊢ (𝑁 ∈ ℕ0
→ ((𝐽 ∈
2ndω ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ) ↔ (𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃
(TopOpen‘(𝔼hil‘𝑁)))))) | 
| 23 | 22 | adantr 480 | . 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ 𝑉) → ((𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ) ↔ (𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃
(TopOpen‘(𝔼hil‘𝑁)))))) | 
| 24 | 1, 23 | bitrd 279 | 1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ 𝑉) → (𝑁ManTop𝐽 ↔ (𝐽 ∈ 2ndω ∧ 𝐽 ∈ Haus ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ≃
(TopOpen‘(𝔼hil‘𝑁)))))) |