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