Theorem acsmre 17740

Description: Algebraic closure systems are closure systems. (Contributed by Stefan O'Rear, 2-Apr-2015.)

Assertion

Ref	Expression
acsmre	⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋))

Proof of Theorem acsmre

Dummy variables 𝑓 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isacs 17739	. 2 ⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))))
2	1	simplbi 502	1 ⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  ∀wral 3076   ∩ cin 3898   ⊆ wss 3899  𝒫 cpw 4557  ∪ cuni 4867   “ cima 5658  ⟶wf 6529  ‘cfv 6533  Fincfn 8952  Moorecmre 17666  ACScacs 17669

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-acs 17673

This theorem is used by:  acsfiel  17742  acsmred  17744  mreacs  17746  isacs3lem  18630  symggen  19597  odf1o1  19699  lsmmod  19802  gsumzsplit  20054  gsumzoppg  20071  gsumpt  20089  dmdprdd  20128  dprdfeq0  20151  dprdspan  20156  dprdres  20157  dprdss  20158  subgdmdprd  20163  subgdprd  20164  dprdsn  20165  dprd2dlem1  20170  dprd2da  20171  dmdprdsplit2lem  20174  ablfac1b  20199  pgpfac1lem1  20203  pgpfac1lem3  20206  pgpfac1lem4  20207  pgpfac1lem5  20208  pgpfaclem2  20211  isnacs2  43551  proot1mul  44035  proot1hash  44036