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=mrCls⁡C
Assertion mrcsscl ⊢C∈Moore⁡X∧U⊆V∧V∈C→F⁡U⊆V

Proof

Step Hyp Ref Expression
1 mrcfval.f ⊢F=mrCls⁡C
2 mress ⊢C∈Moore⁡X∧V∈C→V⊆X
3 2 3adant2 ⊢C∈Moore⁡X∧U⊆V∧V∈C→V⊆X
4 1 mrcss ⊢C∈Moore⁡X∧U⊆V∧V⊆X→F⁡U⊆F⁡V
5 3 4 syld3an3 ⊢C∈Moore⁡X∧U⊆V∧V∈C→F⁡U⊆F⁡V
6 1 mrcid ⊢C∈Moore⁡X∧V∈C→F⁡V=V
7 6 3adant2 ⊢C∈Moore⁡X∧U⊆V∧V∈C→F⁡V=V
8 5 7 sseqtrd ⊢C∈Moore⁡X∧U⊆V∧V∈C→F⁡U⊆V