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 ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑈 ) ⊆ 𝑉 )