Step | Hyp | Ref
| Expression |
1 | | elin 3908 |
. . 3
β’ (πΊ β (Mnd β© TopSp) β
(πΊ β Mnd β§ πΊ β TopSp)) |
2 | 1 | anbi1i 625 |
. 2
β’ ((πΊ β (Mnd β© TopSp) β§
πΉ β ((π½ Γt π½) Cn π½)) β ((πΊ β Mnd β§ πΊ β TopSp) β§ πΉ β ((π½ Γt π½) Cn π½))) |
3 | | fvexd 6815 |
. . . 4
β’ (π = πΊ β (TopOpenβπ) β V) |
4 | | simpl 484 |
. . . . . . 7
β’ ((π = πΊ β§ π = (TopOpenβπ)) β π = πΊ) |
5 | 4 | fveq2d 6804 |
. . . . . 6
β’ ((π = πΊ β§ π = (TopOpenβπ)) β (+πβπ) =
(+πβπΊ)) |
6 | | istmd.1 |
. . . . . 6
β’ πΉ =
(+πβπΊ) |
7 | 5, 6 | eqtr4di 2794 |
. . . . 5
β’ ((π = πΊ β§ π = (TopOpenβπ)) β (+πβπ) = πΉ) |
8 | | id 22 |
. . . . . . . 8
β’ (π = (TopOpenβπ) β π = (TopOpenβπ)) |
9 | | fveq2 6800 |
. . . . . . . . 9
β’ (π = πΊ β (TopOpenβπ) = (TopOpenβπΊ)) |
10 | | istmd.2 |
. . . . . . . . 9
β’ π½ = (TopOpenβπΊ) |
11 | 9, 10 | eqtr4di 2794 |
. . . . . . . 8
β’ (π = πΊ β (TopOpenβπ) = π½) |
12 | 8, 11 | sylan9eqr 2798 |
. . . . . . 7
β’ ((π = πΊ β§ π = (TopOpenβπ)) β π = π½) |
13 | 12, 12 | oveq12d 7321 |
. . . . . 6
β’ ((π = πΊ β§ π = (TopOpenβπ)) β (π Γt π) = (π½ Γt π½)) |
14 | 13, 12 | oveq12d 7321 |
. . . . 5
β’ ((π = πΊ β§ π = (TopOpenβπ)) β ((π Γt π) Cn π) = ((π½ Γt π½) Cn π½)) |
15 | 7, 14 | eleq12d 2831 |
. . . 4
β’ ((π = πΊ β§ π = (TopOpenβπ)) β ((+πβπ) β ((π Γt π) Cn π) β πΉ β ((π½ Γt π½) Cn π½))) |
16 | 3, 15 | sbcied 3766 |
. . 3
β’ (π = πΊ β ([(TopOpenβπ) / π](+πβπ) β ((π Γt π) Cn π) β πΉ β ((π½ Γt π½) Cn π½))) |
17 | | df-tmd 23264 |
. . 3
β’ TopMnd =
{π β (Mnd β© TopSp)
β£ [(TopOpenβπ) / π](+πβπ) β ((π Γt π) Cn π)} |
18 | 16, 17 | elrab2 3632 |
. 2
β’ (πΊ β TopMnd β (πΊ β (Mnd β© TopSp) β§
πΉ β ((π½ Γt π½) Cn π½))) |
19 | | df-3an 1089 |
. 2
β’ ((πΊ β Mnd β§ πΊ β TopSp β§ πΉ β ((π½ Γt π½) Cn π½)) β ((πΊ β Mnd β§ πΊ β TopSp) β§ πΉ β ((π½ Γt π½) Cn π½))) |
20 | 2, 18, 19 | 3bitr4i 304 |
1
β’ (πΊ β TopMnd β (πΊ β Mnd β§ πΊ β TopSp β§ πΉ β ((π½ Γt π½) Cn π½))) |