Theorem mrcss

Description: Closure preserves subset ordering. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypothesis	mrcfval.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion	mrcss	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) ⊆ ( 𝐹 ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2		sstr2	⊢ ( 𝑈 ⊆ 𝑉 → ( 𝑉 ⊆ 𝑠 → 𝑈 ⊆ 𝑠 ) )
3	2	adantr	⊢ ( ( 𝑈 ⊆ 𝑉 ∧ 𝑠 ∈ 𝐶 ) → ( 𝑉 ⊆ 𝑠 → 𝑈 ⊆ 𝑠 ) )
4	3	ss2rabdv	⊢ ( 𝑈 ⊆ 𝑉 → { 𝑠 ∈ 𝐶 ∣ 𝑉 ⊆ 𝑠 } ⊆ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } )
5		intss	⊢ ( { 𝑠 ∈ 𝐶 ∣ 𝑉 ⊆ 𝑠 } ⊆ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ⊆ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑉 ⊆ 𝑠 } )
6	4 5	syl	⊢ ( 𝑈 ⊆ 𝑉 → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ⊆ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑉 ⊆ 𝑠 } )
7	6	3ad2ant2	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ⊆ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑉 ⊆ 𝑠 } )
8		simp1	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
9		sstr	⊢ ( ( 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → 𝑈 ⊆ 𝑋 )
10	9	3adant1	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → 𝑈 ⊆ 𝑋 )
11	1	mrcval	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } )
12	8 10 11	syl2anc	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } )
13	1	mrcval	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑉 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑉 ⊆ 𝑠 } )
14	13	3adant2	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑉 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑉 ⊆ 𝑠 } )
15	7 12 14	3sstr4d	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) ⊆ ( 𝐹 ‘ 𝑉 ) )