Step | Hyp | Ref
| Expression |
1 | | elin 3758 |
. . 3
⊢ (𝐺 ∈ (Mnd ∩ TopSp) ↔
(𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp)) |
2 | 1 | anbi1i 727 |
. 2
⊢ ((𝐺 ∈ (Mnd ∩ TopSp) ∧
𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) ↔ ((𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp) ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))) |
3 | | fvex 6113 |
. . . . 5
⊢
(TopOpen‘𝑓)
∈ V |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝑓 = 𝐺 → (TopOpen‘𝑓) ∈ V) |
5 | | simpl 472 |
. . . . . . 7
⊢ ((𝑓 = 𝐺 ∧ 𝑗 = (TopOpen‘𝑓)) → 𝑓 = 𝐺) |
6 | 5 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑓 = 𝐺 ∧ 𝑗 = (TopOpen‘𝑓)) → (+𝑓‘𝑓) =
(+𝑓‘𝐺)) |
7 | | istmd.1 |
. . . . . 6
⊢ 𝐹 =
(+𝑓‘𝐺) |
8 | 6, 7 | syl6eqr 2662 |
. . . . 5
⊢ ((𝑓 = 𝐺 ∧ 𝑗 = (TopOpen‘𝑓)) → (+𝑓‘𝑓) = 𝐹) |
9 | | id 22 |
. . . . . . . 8
⊢ (𝑗 = (TopOpen‘𝑓) → 𝑗 = (TopOpen‘𝑓)) |
10 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑓 = 𝐺 → (TopOpen‘𝑓) = (TopOpen‘𝐺)) |
11 | | istmd.2 |
. . . . . . . . 9
⊢ 𝐽 = (TopOpen‘𝐺) |
12 | 10, 11 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑓 = 𝐺 → (TopOpen‘𝑓) = 𝐽) |
13 | 9, 12 | sylan9eqr 2666 |
. . . . . . 7
⊢ ((𝑓 = 𝐺 ∧ 𝑗 = (TopOpen‘𝑓)) → 𝑗 = 𝐽) |
14 | 13, 13 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑓 = 𝐺 ∧ 𝑗 = (TopOpen‘𝑓)) → (𝑗 ×t 𝑗) = (𝐽 ×t 𝐽)) |
15 | 14, 13 | oveq12d 6567 |
. . . . 5
⊢ ((𝑓 = 𝐺 ∧ 𝑗 = (TopOpen‘𝑓)) → ((𝑗 ×t 𝑗) Cn 𝑗) = ((𝐽 ×t 𝐽) Cn 𝐽)) |
16 | 8, 15 | eleq12d 2682 |
. . . 4
⊢ ((𝑓 = 𝐺 ∧ 𝑗 = (TopOpen‘𝑓)) → ((+𝑓‘𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗) ↔ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))) |
17 | 4, 16 | sbcied 3439 |
. . 3
⊢ (𝑓 = 𝐺 → ([(TopOpen‘𝑓) / 𝑗](+𝑓‘𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗) ↔ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))) |
18 | | df-tmd 21686 |
. . 3
⊢ TopMnd =
{𝑓 ∈ (Mnd ∩ TopSp)
∣ [(TopOpen‘𝑓) / 𝑗](+𝑓‘𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗)} |
19 | 17, 18 | elrab2 3333 |
. 2
⊢ (𝐺 ∈ TopMnd ↔ (𝐺 ∈ (Mnd ∩ TopSp) ∧
𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))) |
20 | | df-3an 1033 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) ↔ ((𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp) ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))) |
21 | 2, 19, 20 | 3bitr4i 291 |
1
⊢ (𝐺 ∈ TopMnd ↔ (𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))) |