Metamath Proof Explorer


Theorem istmd

Description: The predicate "is a topological monoid". (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypotheses istmd.1
|- F = ( +f ` G )
istmd.2
|- J = ( TopOpen ` G )
Assertion istmd
|- ( G e. TopMnd <-> ( G e. Mnd /\ G e. TopSp /\ F e. ( ( J tX J ) Cn J ) ) )

Proof

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 ) ) )