Step | Hyp | Ref
| Expression |
1 | | simpl 475 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑗 = 𝐽) → 𝑛 = 𝑁) |
2 | 1 | eleq1d 2863 |
. . . 4
⊢ ((𝑛 = 𝑁 ∧ 𝑗 = 𝐽) → (𝑛 ∈ ℕ0 ↔ 𝑁 ∈
ℕ0)) |
3 | | simpr 478 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑗 = 𝐽) → 𝑗 = 𝐽) |
4 | 3 | eleq1d 2863 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑗 = 𝐽) → (𝑗 ∈ 2nd𝜔 ↔ 𝐽 ∈
2nd𝜔)) |
5 | 3 | eleq1d 2863 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑗 = 𝐽) → (𝑗 ∈ Haus ↔ 𝐽 ∈ Haus)) |
6 | | 2fveq3 6416 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 →
(TopOpen‘(𝔼hil‘𝑛)) =
(TopOpen‘(𝔼hil‘𝑁))) |
7 | 6 | eceq1d 8021 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 →
[(TopOpen‘(𝔼hil‘𝑛))] ≃ =
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ) |
8 | | llyeq 21602 |
. . . . . . . 8
⊢
([(TopOpen‘(𝔼hil‘𝑛))] ≃ =
[(TopOpen‘(𝔼hil‘𝑁))] ≃ → Locally
[(TopOpen‘(𝔼hil‘𝑛))] ≃ = Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → Locally
[(TopOpen‘(𝔼hil‘𝑛))] ≃ = Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ) |
10 | 9 | adantr 473 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑗 = 𝐽) → Locally
[(TopOpen‘(𝔼hil‘𝑛))] ≃ = Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ) |
11 | 3, 10 | eleq12d 2872 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑗 = 𝐽) → (𝑗 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑛))] ≃ ↔ 𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ )) |
12 | 4, 5, 11 | 3anbi123d 1561 |
. . . 4
⊢ ((𝑛 = 𝑁 ∧ 𝑗 = 𝐽) → ((𝑗 ∈ 2nd𝜔 ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑛))] ≃ ) ↔ (𝐽 ∈ 2nd𝜔 ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ))) |
13 | 2, 12 | anbi12d 625 |
. . 3
⊢ ((𝑛 = 𝑁 ∧ 𝑗 = 𝐽) → ((𝑛 ∈ ℕ0 ∧ (𝑗 ∈ 2nd𝜔
∧ 𝑗 ∈ Haus ∧
𝑗 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑛))] ≃ )) ↔ (𝑁 ∈ ℕ0 ∧ (𝐽 ∈ 2nd𝜔
∧ 𝐽 ∈ Haus ∧
𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ )))) |
14 | | df-mntop 30583 |
. . 3
⊢ ManTop =
{〈𝑛, 𝑗〉 ∣ (𝑛 ∈ ℕ0
∧ (𝑗 ∈
2nd𝜔 ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑛))] ≃ ))} |
15 | 13, 14 | brabga 5185 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ 𝑉) → (𝑁ManTop𝐽 ↔ (𝑁 ∈ ℕ0 ∧ (𝐽 ∈ 2nd𝜔
∧ 𝐽 ∈ Haus ∧
𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ )))) |
16 | | simpl 475 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ 𝑉) → 𝑁 ∈
ℕ0) |
17 | 16 | biantrurd 529 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ 𝑉) → ((𝐽 ∈ 2nd𝜔 ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ) ↔ (𝑁 ∈ ℕ0 ∧ (𝐽 ∈ 2nd𝜔
∧ 𝐽 ∈ Haus ∧
𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ )))) |
18 | 15, 17 | bitr4d 274 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐽 ∈ 𝑉) → (𝑁ManTop𝐽 ↔ (𝐽 ∈ 2nd𝜔 ∧ 𝐽 ∈ Haus ∧ 𝐽 ∈ Locally
[(TopOpen‘(𝔼hil‘𝑁))] ≃ ))) |