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