MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  istmd Structured version   Visualization version   GIF version

Theorem istmd 21788
Description: The predicate "is a topological monoid". (Contributed by Mario Carneiro, 19-Sep-2015.)
Hypotheses
Ref Expression
istmd.1 𝐹 = (+𝑓𝐺)
istmd.2 𝐽 = (TopOpen‘𝐺)
Assertion
Ref Expression
istmd (𝐺 ∈ TopMnd ↔ (𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)))

Proof of Theorem istmd
Dummy variables 𝑓 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elin 3774 . . 3 (𝐺 ∈ (Mnd ∩ TopSp) ↔ (𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp))
21anbi1i 730 . 2 ((𝐺 ∈ (Mnd ∩ TopSp) ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) ↔ ((𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp) ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)))
3 fvex 6158 . . . . 5 (TopOpen‘𝑓) ∈ V
43a1i 11 . . . 4 (𝑓 = 𝐺 → (TopOpen‘𝑓) ∈ V)
5 simpl 473 . . . . . . 7 ((𝑓 = 𝐺𝑗 = (TopOpen‘𝑓)) → 𝑓 = 𝐺)
65fveq2d 6152 . . . . . 6 ((𝑓 = 𝐺𝑗 = (TopOpen‘𝑓)) → (+𝑓𝑓) = (+𝑓𝐺))
7 istmd.1 . . . . . 6 𝐹 = (+𝑓𝐺)
86, 7syl6eqr 2673 . . . . 5 ((𝑓 = 𝐺𝑗 = (TopOpen‘𝑓)) → (+𝑓𝑓) = 𝐹)
9 id 22 . . . . . . . 8 (𝑗 = (TopOpen‘𝑓) → 𝑗 = (TopOpen‘𝑓))
10 fveq2 6148 . . . . . . . . 9 (𝑓 = 𝐺 → (TopOpen‘𝑓) = (TopOpen‘𝐺))
11 istmd.2 . . . . . . . . 9 𝐽 = (TopOpen‘𝐺)
1210, 11syl6eqr 2673 . . . . . . . 8 (𝑓 = 𝐺 → (TopOpen‘𝑓) = 𝐽)
139, 12sylan9eqr 2677 . . . . . . 7 ((𝑓 = 𝐺𝑗 = (TopOpen‘𝑓)) → 𝑗 = 𝐽)
1413, 13oveq12d 6622 . . . . . 6 ((𝑓 = 𝐺𝑗 = (TopOpen‘𝑓)) → (𝑗 ×t 𝑗) = (𝐽 ×t 𝐽))
1514, 13oveq12d 6622 . . . . 5 ((𝑓 = 𝐺𝑗 = (TopOpen‘𝑓)) → ((𝑗 ×t 𝑗) Cn 𝑗) = ((𝐽 ×t 𝐽) Cn 𝐽))
168, 15eleq12d 2692 . . . 4 ((𝑓 = 𝐺𝑗 = (TopOpen‘𝑓)) → ((+𝑓𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗) ↔ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)))
174, 16sbcied 3454 . . 3 (𝑓 = 𝐺 → ([(TopOpen‘𝑓) / 𝑗](+𝑓𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗) ↔ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)))
18 df-tmd 21786 . . 3 TopMnd = {𝑓 ∈ (Mnd ∩ TopSp) ∣ [(TopOpen‘𝑓) / 𝑗](+𝑓𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗)}
1917, 18elrab2 3348 . 2 (𝐺 ∈ TopMnd ↔ (𝐺 ∈ (Mnd ∩ TopSp) ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)))
20 df-3an 1038 . 2 ((𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) ↔ ((𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp) ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)))
212, 19, 203bitr4i 292 1 (𝐺 ∈ TopMnd ↔ (𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  Vcvv 3186  [wsbc 3417  cin 3554  cfv 5847  (class class class)co 6604  TopOpenctopn 16003  +𝑓cplusf 17160  Mndcmnd 17215  TopSpctps 20619   Cn ccn 20938   ×t ctx 21273  TopMndctmd 21784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4749
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-iota 5810  df-fv 5855  df-ov 6607  df-tmd 21786
This theorem is referenced by:  tmdmnd  21789  tmdtps  21790  tmdcn  21797  istgp2  21805  oppgtmd  21811  symgtgp  21815  submtmd  21818  prdstmdd  21837  nrgtrg  22404  mhmhmeotmd  29755  xrge0tmdOLD  29773
  Copyright terms: Public domain W3C validator