| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mresspw | Structured version Visualization version GIF version | ||
| Description: A Moore collection is a subset of the power of the base set; each closed subset of the system is actually a subset of the base. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| Ref | Expression |
|---|---|
| mresspw | ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐶 ⊆ 𝒫 𝑋) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ismre 17667 | . 2 ⊢ (𝐶 ∈ (Moore‘𝑋) ↔ (𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀𝑠 ∈ 𝒫 𝐶(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶))) | |
| 2 | 1 | simp1bi 1163 | 1 ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐶 ⊆ 𝒫 𝑋) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∈ wcel 2146 ≠ wne 2961 ∀wral 3082 ⊆ wss 3908 ∅c0 4289 𝒫 cpw 4567 ∩ cint 4917 ‘cfv 6543 Moorecmre 17659 |
| 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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 |
| 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 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-ral 3083 df-rex 3093 df-rab 3420 df-v 3460 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-br 5115 df-opab 5179 df-mpt 5198 df-id 5561 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-iota 6499 df-fun 6545 df-fv 6551 df-mre 17663 |
| This theorem is used by: mress 17670 mrerintcl 17674 mreuni 17677 mremre 17681 isacs2 17734 mreacs 17739 isacs3lem 18623 dmdprdd 20096 dprdfeq0 20119 dprdss 20126 dprdz 20127 subgdmdprd 20131 subgdprd 20132 dprd2dlem1 20138 dprd2da 20139 dmdprdsplit2lem 20142 mretopd 23279 ismrc 43465 |
| Copyright terms: Public domain | W3C validator |