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 ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion mrcsscl ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑈 ) ⊆ 𝑉 )

Proof

Step Hyp Ref Expression
1 mrcfval.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2 mress ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑉 ∈ 𝐶 ) → 𝑉 ⊆ 𝑋 )
3 2 3adant2 ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ∈ 𝐶 ) → 𝑉 ⊆ 𝑋 )
4 1 mrcss ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) ⊆ ( 𝐹 ‘ 𝑉 ) )
5 3 4 syld3an3 ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑈 ) ⊆ ( 𝐹 ‘ 𝑉 ) )
6 1 mrcid ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑉 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑉 ) = 𝑉 )
7 6 3adant2 ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑉 ) = 𝑉 )
8 5 7 sseqtrd ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑈 ) ⊆ 𝑉 )