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