Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mrcsscl | Structured version Visualization version GIF version |
Description: The closure is the minimal closed set; any closed set which contains the generators is a superset of the closure. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
Ref | Expression |
---|---|
mrcfval.f | β’ πΉ = (mrClsβπΆ) |
Ref | Expression |
---|---|
mrcsscl | β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β πΆ) β (πΉβπ) β π) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mress 17399 | . . . 4 β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β π β π) | |
2 | 1 | 3adant2 1130 | . . 3 β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β πΆ) β π β π) |
3 | mrcfval.f | . . . 4 β’ πΉ = (mrClsβπΆ) | |
4 | 3 | mrcss 17422 | . . 3 β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β (πΉβπ) β (πΉβπ)) |
5 | 2, 4 | syld3an3 1408 | . 2 β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β πΆ) β (πΉβπ) β (πΉβπ)) |
6 | 3 | mrcid 17419 | . . 3 β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β (πΉβπ) = π) |
7 | 6 | 3adant2 1130 | . 2 β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β πΆ) β (πΉβπ) = π) |
8 | 5, 7 | sseqtrd 3972 | 1 β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β πΆ) β (πΉβπ) β π) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ w3a 1086 = wceq 1540 β wcel 2105 β wss 3898 βcfv 6479 Moorecmre 17388 mrClscmrc 17389 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-sep 5243 ax-nul 5250 ax-pow 5308 ax-pr 5372 ax-un 7650 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3404 df-v 3443 df-sbc 3728 df-csb 3844 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4270 df-if 4474 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4853 df-int 4895 df-br 5093 df-opab 5155 df-mpt 5176 df-id 5518 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-iota 6431 df-fun 6481 df-fn 6482 df-f 6483 df-fv 6487 df-mre 17392 df-mrc 17393 |
This theorem is referenced by: submrc 17434 isacs2 17459 isacs3lem 18357 mrelatlub 18377 mndind 18563 gsumwspan 18581 symggen 19174 cntzspan 19540 dprdspan 19725 subgdmdprd 19732 subgdprd 19733 dprdsn 19734 dprd2dlem1 19739 dprd2da 19740 dmdprdsplit2lem 19743 ablfac1b 19768 pgpfac1lem1 19772 pgpfac1lem5 19777 mrccss 21005 evlseu 21399 ismrcd2 40783 mrefg3 40792 isnacs3 40794 |
Copyright terms: Public domain | W3C validator |