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 = + 𝑓 G
istmd.2 J = TopOpen G
Assertion istmd G TopMnd G Mnd G TopSp F J × t J Cn J

Proof

Step Hyp Ref Expression
1 istmd.1 F = + 𝑓 G
2 istmd.2 J = TopOpen G
3 elin G Mnd TopSp G Mnd G TopSp
4 3 anbi1i G Mnd TopSp F J × t J Cn J G Mnd G TopSp F J × t J Cn J
5 fvexd f = G TopOpen f V
6 simpl f = G j = TopOpen f f = G
7 6 fveq2d f = G j = TopOpen f + 𝑓 f = + 𝑓 G
8 7 1 eqtr4di f = G j = TopOpen 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 × t j = J × t J
14 13 12 oveq12d f = G j = TopOpen f j × t j Cn j = J × t J Cn J
15 8 14 eleq12d f = G j = TopOpen f + 𝑓 f j × t j Cn j F J × t J Cn J
16 5 15 sbcied f = G [˙ TopOpen f / j]˙ + 𝑓 f j × t j Cn j F J × t J Cn J
17 df-tmd TopMnd = f Mnd TopSp | [˙ TopOpen f / j]˙ + 𝑓 f j × t j Cn j
18 16 17 elrab2 G TopMnd G Mnd TopSp F J × t J Cn J
19 df-3an G Mnd G TopSp F J × t J Cn J G Mnd G TopSp F J × t J Cn J
20 4 18 19 3bitr4i G TopMnd G Mnd G TopSp F J × t J Cn J