![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > acsmre | Structured version Visualization version GIF version |
Description: Algebraic closure systems are closure systems. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
Ref | Expression |
---|---|
acsmre | ⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isacs 16623 | . 2 ⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)))) | |
2 | 1 | simplbi 492 | 1 ⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 385 ∃wex 1875 ∈ wcel 2157 ∀wral 3087 ∩ cin 3766 ⊆ wss 3767 𝒫 cpw 4347 ∪ cuni 4626 “ cima 5313 ⟶wf 6095 ‘cfv 6099 Fincfn 8193 Moorecmre 16554 ACScacs 16557 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-sep 4973 ax-nul 4981 ax-pow 5033 ax-pr 5095 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ral 3092 df-rex 3093 df-rab 3096 df-v 3385 df-sbc 3632 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-nul 4114 df-if 4276 df-pw 4349 df-sn 4367 df-pr 4369 df-op 4373 df-uni 4627 df-br 4842 df-opab 4904 df-mpt 4921 df-id 5218 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-dm 5320 df-rn 5321 df-iota 6062 df-fun 6101 df-fn 6102 df-f 6103 df-fv 6107 df-acs 16561 |
This theorem is referenced by: acsfiel 16626 acsmred 16628 mreacs 16630 isacs3lem 17478 symggen 18199 odf1o1 18297 lsmmod 18398 gsumzsplit 18639 gsumzoppg 18656 gsumpt 18673 dmdprdd 18711 dprdfeq0 18734 dprdspan 18739 dprdres 18740 dprdss 18741 subgdmdprd 18746 subgdprd 18747 dprdsn 18748 dprd2dlem1 18753 dprd2da 18754 dmdprdsplit2lem 18757 ablfac1b 18782 pgpfac1lem1 18786 pgpfac1lem3 18789 pgpfac1lem4 18790 pgpfac1lem5 18791 pgpfaclem1 18793 pgpfaclem2 18794 isnacs2 38043 proot1mul 38550 proot1hash 38551 |
Copyright terms: Public domain | W3C validator |