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