# Metamath Proof Explorer

## Theorem mrcsscl

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
Hypothesis mrcfval.f ${⊢}{F}=\mathrm{mrCls}\left({C}\right)$
Assertion mrcsscl ${⊢}\left({C}\in \mathrm{Moore}\left({X}\right)\wedge {U}\subseteq {V}\wedge {V}\in {C}\right)\to {F}\left({U}\right)\subseteq {V}$

### Proof

Step Hyp Ref Expression
1 mrcfval.f ${⊢}{F}=\mathrm{mrCls}\left({C}\right)$
2 mress ${⊢}\left({C}\in \mathrm{Moore}\left({X}\right)\wedge {V}\in {C}\right)\to {V}\subseteq {X}$
3 2 3adant2 ${⊢}\left({C}\in \mathrm{Moore}\left({X}\right)\wedge {U}\subseteq {V}\wedge {V}\in {C}\right)\to {V}\subseteq {X}$
4 1 mrcss ${⊢}\left({C}\in \mathrm{Moore}\left({X}\right)\wedge {U}\subseteq {V}\wedge {V}\subseteq {X}\right)\to {F}\left({U}\right)\subseteq {F}\left({V}\right)$
5 3 4 syld3an3 ${⊢}\left({C}\in \mathrm{Moore}\left({X}\right)\wedge {U}\subseteq {V}\wedge {V}\in {C}\right)\to {F}\left({U}\right)\subseteq {F}\left({V}\right)$
6 1 mrcid ${⊢}\left({C}\in \mathrm{Moore}\left({X}\right)\wedge {V}\in {C}\right)\to {F}\left({V}\right)={V}$
7 6 3adant2 ${⊢}\left({C}\in \mathrm{Moore}\left({X}\right)\wedge {U}\subseteq {V}\wedge {V}\in {C}\right)\to {F}\left({V}\right)={V}$
8 5 7 sseqtrd ${⊢}\left({C}\in \mathrm{Moore}\left({X}\right)\wedge {U}\subseteq {V}\wedge {V}\in {C}\right)\to {F}\left({U}\right)\subseteq {V}$