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

Theorem acsmre 14602
Description: Algebraic closure systems are closure systems. (Contributed by Stefan O'Rear, 2-Apr-2015.)
Assertion
Ref Expression
acsmre  |-  ( C  e.  (ACS `  X
)  ->  C  e.  (Moore `  X ) )

Proof of Theorem acsmre
Dummy variables  f 
s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isacs 14601 . 2  |-  ( C  e.  (ACS `  X
)  <->  ( C  e.  (Moore `  X )  /\  E. f ( f : ~P X --> ~P X  /\  A. s  e.  ~P  X ( s  e.  C  <->  U. ( f "
( ~P s  i^i 
Fin ) )  C_  s ) ) ) )
21simplbi 460 1  |-  ( C  e.  (ACS `  X
)  ->  C  e.  (Moore `  X ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   E.wex 1586    e. wcel 1756   A.wral 2727    i^i cin 3339    C_ wss 3340   ~Pcpw 3872   U.cuni 4103   "cima 4855   -->wf 5426   ` cfv 5430   Fincfn 7322  Moorecmre 14532  ACScacs 14535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-sbc 3199  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-mpt 4364  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-fv 5438  df-acs 14539
This theorem is referenced by:  acsfiel  14604  acsmred  14606  mreacs  14608  isacs3lem  15348  symggen  15988  odf1o1  16083  lsmmod  16184  gsumzsplit  16430  gsumzsplitOLD  16431  gsumzoppg  16452  gsumzoppgOLD  16453  gsumpt  16466  gsumptOLD  16467  dmdprdd  16493  dprdfeq0  16524  dprdfeq0OLD  16531  dprdspan  16536  dprdres  16537  dprdss  16538  subgdmdprd  16543  subgdprd  16544  dprdsn  16545  dprd2dlem1  16552  dprd2da  16553  dmdprdsplit2lem  16556  ablfac1b  16583  pgpfac1lem1  16587  pgpfac1lem3  16590  pgpfac1lem4  16591  pgpfac1lem5  16592  pgpfaclem1  16594  pgpfaclem2  16595  isnacs2  29054  proot1mul  29576  proot1hash  29580
  Copyright terms: Public domain W3C validator