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

Theorem pgpgrp 18830
Description: Reverse closure for the second argument of pGrp. (Contributed by Mario Carneiro, 15-Jan-2015.)
Assertion
Ref Expression
pgpgrp (𝑃 pGrp 𝐺𝐺 ∈ Grp)

Proof of Theorem pgpgrp
Dummy variables 𝑥 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2738 . . 3 (Base‘𝐺) = (Base‘𝐺)
2 eqid 2738 . . 3 (od‘𝐺) = (od‘𝐺)
31, 2ispgp 18828 . 2 (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀𝑥 ∈ (Base‘𝐺)∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃𝑛)))
43simp2bi 1147 1 (𝑃 pGrp 𝐺𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2113  wral 3053  wrex 3054   class class class wbr 5027  cfv 6333  (class class class)co 7164  0cn0 11969  cexp 13514  cprime 16105  Basecbs 16579  Grpcgrp 18212  odcod 18763   pGrp cpgp 18765
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-v 3399  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-br 5028  df-opab 5090  df-xp 5525  df-iota 6291  df-fv 6341  df-ov 7167  df-pgp 18769
This theorem is referenced by:  pgphash  18843
  Copyright terms: Public domain W3C validator