![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mrccl | Structured version Visualization version GIF version |
Description: The Moore closure of a set is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
Ref | Expression |
---|---|
mrcfval.f | ⊢ 𝐹 = (mrCls‘𝐶) |
Ref | Expression |
---|---|
mrccl | ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘𝑈) ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mrcfval.f | . . . 4 ⊢ 𝐹 = (mrCls‘𝐶) | |
2 | 1 | mrcf 16713 | . . 3 ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝐶) |
3 | 2 | adantr 481 | . 2 ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → 𝐹:𝒫 𝑋⟶𝐶) |
4 | mre1cl 16698 | . . . 4 ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝑋 ∈ 𝐶) | |
5 | elpw2g 5145 | . . . 4 ⊢ (𝑋 ∈ 𝐶 → (𝑈 ∈ 𝒫 𝑋 ↔ 𝑈 ⊆ 𝑋)) | |
6 | 4, 5 | syl 17 | . . 3 ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑈 ∈ 𝒫 𝑋 ↔ 𝑈 ⊆ 𝑋)) |
7 | 6 | biimpar 478 | . 2 ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → 𝑈 ∈ 𝒫 𝑋) |
8 | 3, 7 | ffvelrnd 6724 | 1 ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘𝑈) ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1525 ∈ wcel 2083 ⊆ wss 3865 𝒫 cpw 4459 ⟶wf 6228 ‘cfv 6232 Moorecmre 16686 mrClscmrc 16687 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-ral 3112 df-rex 3113 df-rab 3116 df-v 3442 df-sbc 3712 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-int 4789 df-br 4969 df-opab 5031 df-mpt 5048 df-id 5355 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-fv 6240 df-mre 16690 df-mrc 16691 |
This theorem is referenced by: mrcsncl 16716 mrcidb 16719 mrcidm 16723 submrc 16732 isacs2 16757 mrelatlub 17629 mreclatBAD 17630 gsumwspan 17826 cycsubg2cl 18075 symggen 18333 odf1o1 18431 cntzspan 18691 gsumzsplit 18771 gsumzoppg 18788 gsumpt 18806 dmdprdd 18842 dprdfeq0 18865 dprdspan 18870 dprdres 18871 dprdz 18873 subgdmdprd 18877 subgdprd 18878 dprd2dlem1 18884 dprd2da 18885 dmdprdsplit2lem 18888 mrccss 20524 ismrcd2 38802 proot1mul 39305 |
Copyright terms: Public domain | W3C validator |