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

Metamath Proof Explorer

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