Nearby theorems
|
|
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 17559 | . . 3 β’ (πΆ β (Mooreβπ) β πΉ:π« πβΆπΆ) |
| 3 | 2 | adantr 479 | . 2 β’ ((πΆ β (Mooreβπ) β§ π β π) β πΉ:π« πβΆπΆ) |
| 4 | mre1cl 17544 | . . . 4 β’ (πΆ β (Mooreβπ) β π β πΆ) | |
| 5 | elpw2g 5345 | . . . 4 β’ (π β πΆ β (π β π« π β π β π)) | |
| 6 | 4, 5 | syl 17 | . . 3 β’ (πΆ β (Mooreβπ) β (π β π« π β π β π)) |
| 7 | 6 | biimpar 476 | . 2 β’ ((πΆ β (Mooreβπ) β§ π β π) β π β π« π) |
| 8 | 3, 7 | ffvelcdmd 7088 | 1 β’ ((πΆ β (Mooreβπ) β§ π β π) β (πΉβπ) β πΆ) |
| Colors of variables: wff setvar class |
| Syntax hints: β wi 4 β wb 205 β§ wa 394 = wceq 1539 β wcel 2104 β wss 3949 π« cpw 4603 βΆwf 6540 βcfv 6544 Moorecmre 17532 mrClscmrc 17533 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7729 |
| This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-int 4952 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-fv 6552 df-mre 17536 df-mrc 17537 |
| This theorem is referenced by: mrcsncl 17562 mrcidb 17565 mrcidm 17569 submrc 17578 isacs2 17603 mrelatlub 18521 mreclatBAD 18522 gsumwspan 18765 cycsubg2cl 19128 symggen 19381 odf1o1 19483 cntzspan 19755 gsumzsplit 19838 gsumzoppg 19855 gsumpt 19873 dmdprdd 19912 dprdfeq0 19935 dprdspan 19940 dprdres 19941 dprdz 19943 subgdmdprd 19947 subgdprd 19948 dprd2dlem1 19954 dprd2da 19955 dmdprdsplit2lem 19958 mrccss 21468 ismrcd2 41741 proot1mul 42245 mrelatlubALT 47709 mreclat 47711 |
| Copyright terms: Public domain | W3C validator |