This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. ( Moore ` X ) /\ U C_ V /\ V e. C ) -> ( F ` U ) C_ V )

Proof

Step Hyp Ref Expression
1 mrcfval.f 
 |-  F = ( mrCls ` C )
2 mress 
 |-  ( ( C e. ( Moore ` X ) /\ V e. C ) -> V C_ X )
3 2 3adant2 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ V /\ V e. C ) -> V C_ X )
4 1 mrcss 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ V /\ V C_ X ) -> ( F ` U ) C_ ( F ` V ) )
5 3 4 syld3an3 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ V /\ V e. C ) -> ( F ` U ) C_ ( F ` V ) )
6 1 mrcid 
 |-  ( ( C e. ( Moore ` X ) /\ V e. C ) -> ( F ` V ) = V )
7 6 3adant2 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ V /\ V e. C ) -> ( F ` V ) = V )
8 5 7 sseqtrd 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ V /\ V e. C ) -> ( F ` U ) C_ V )