Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  grpomndo Structured version   Unicode version

Theorem grpomndo 26016
 Description: A group is a monoid. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
Assertion
Ref Expression
grpomndo MndOp

Proof of Theorem grpomndo
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2428 . . . . 5
21isgrpo 25866 . . . 4
32biimpd 210 . . 3
41grpoidinv 25878 . . . . . . . 8
5 simpl 458 . . . . . . . . . . 11
65ralimi 2758 . . . . . . . . . 10
76reximi 2832 . . . . . . . . 9
81ismndo2 26015 . . . . . . . . . . . . 13 MndOp
98biimprcd 228 . . . . . . . . . . . 12 MndOp
1093exp 1204 . . . . . . . . . . 11 MndOp
1110impcom 431 . . . . . . . . . 10 MndOp
1211com3l 84 . . . . . . . . 9 MndOp
137, 12syl 17 . . . . . . . 8 MndOp
144, 13mpcom 37 . . . . . . 7 MndOp
1514expdcom 440 . . . . . 6 MndOp
1615a1i 11 . . . . 5 MndOp
1716com13 83 . . . 4 MndOp
18173imp 1199 . . 3 MndOp
193, 18syli 38 . 2 MndOp
2019pm2.43i 49 1 MndOp
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   w3a 982   wceq 1437   wcel 1872  wral 2714  wrex 2715   cxp 4794   crn 4797  wf 5540  (class class class)co 6249  cgr 25856  MndOpcmndo 26007 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603  ax-un 6541 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-fo 5550  df-fv 5552  df-ov 6252  df-grpo 25861  df-ass 25983  df-exid 25985  df-mgmOLD 25989  df-sgrOLD 26001  df-mndo 26008 This theorem is referenced by:  isdrngo2  32104
 Copyright terms: Public domain W3C validator