Step |
Hyp |
Ref |
Expression |
1 |
|
istmd.1 |
|- F = ( +f ` G ) |
2 |
|
istmd.2 |
|- J = ( TopOpen ` G ) |
3 |
|
elin |
|- ( G e. ( Mnd i^i TopSp ) <-> ( G e. Mnd /\ G e. TopSp ) ) |
4 |
3
|
anbi1i |
|- ( ( G e. ( Mnd i^i TopSp ) /\ F e. ( ( J tX J ) Cn J ) ) <-> ( ( G e. Mnd /\ G e. TopSp ) /\ F e. ( ( J tX J ) Cn J ) ) ) |
5 |
|
fvexd |
|- ( f = G -> ( TopOpen ` f ) e. _V ) |
6 |
|
simpl |
|- ( ( f = G /\ j = ( TopOpen ` f ) ) -> f = G ) |
7 |
6
|
fveq2d |
|- ( ( f = G /\ j = ( TopOpen ` f ) ) -> ( +f ` f ) = ( +f ` G ) ) |
8 |
7 1
|
eqtr4di |
|- ( ( f = G /\ j = ( TopOpen ` f ) ) -> ( +f ` f ) = F ) |
9 |
|
id |
|- ( j = ( TopOpen ` f ) -> j = ( TopOpen ` f ) ) |
10 |
|
fveq2 |
|- ( f = G -> ( TopOpen ` f ) = ( TopOpen ` G ) ) |
11 |
10 2
|
eqtr4di |
|- ( f = G -> ( TopOpen ` f ) = J ) |
12 |
9 11
|
sylan9eqr |
|- ( ( f = G /\ j = ( TopOpen ` f ) ) -> j = J ) |
13 |
12 12
|
oveq12d |
|- ( ( f = G /\ j = ( TopOpen ` f ) ) -> ( j tX j ) = ( J tX J ) ) |
14 |
13 12
|
oveq12d |
|- ( ( f = G /\ j = ( TopOpen ` f ) ) -> ( ( j tX j ) Cn j ) = ( ( J tX J ) Cn J ) ) |
15 |
8 14
|
eleq12d |
|- ( ( f = G /\ j = ( TopOpen ` f ) ) -> ( ( +f ` f ) e. ( ( j tX j ) Cn j ) <-> F e. ( ( J tX J ) Cn J ) ) ) |
16 |
5 15
|
sbcied |
|- ( f = G -> ( [. ( TopOpen ` f ) / j ]. ( +f ` f ) e. ( ( j tX j ) Cn j ) <-> F e. ( ( J tX J ) Cn J ) ) ) |
17 |
|
df-tmd |
|- TopMnd = { f e. ( Mnd i^i TopSp ) | [. ( TopOpen ` f ) / j ]. ( +f ` f ) e. ( ( j tX j ) Cn j ) } |
18 |
16 17
|
elrab2 |
|- ( G e. TopMnd <-> ( G e. ( Mnd i^i TopSp ) /\ F e. ( ( J tX J ) Cn J ) ) ) |
19 |
|
df-3an |
|- ( ( G e. Mnd /\ G e. TopSp /\ F e. ( ( J tX J ) Cn J ) ) <-> ( ( G e. Mnd /\ G e. TopSp ) /\ F e. ( ( J tX J ) Cn J ) ) ) |
20 |
4 18 19
|
3bitr4i |
|- ( G e. TopMnd <-> ( G e. Mnd /\ G e. TopSp /\ F e. ( ( J tX J ) Cn J ) ) ) |