Metamath Proof Explorer


Theorem pclssN

Description: Ordering is preserved by subspace closure. (Contributed by NM, 8-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pclss.a 𝐴 = ( Atoms ‘ 𝐾 )
pclss.c 𝑈 = ( PCl ‘ 𝐾 )
Assertion pclssN ( ( 𝐾𝑉𝑋𝑌𝑌𝐴 ) → ( 𝑈𝑋 ) ⊆ ( 𝑈𝑌 ) )

Proof

Step Hyp Ref Expression
1 pclss.a 𝐴 = ( Atoms ‘ 𝐾 )
2 pclss.c 𝑈 = ( PCl ‘ 𝐾 )
3 sstr2 ( 𝑋𝑌 → ( 𝑌𝑦𝑋𝑦 ) )
4 3 3ad2ant2 ( ( 𝐾𝑉𝑋𝑌𝑌𝐴 ) → ( 𝑌𝑦𝑋𝑦 ) )
5 4 adantr ( ( ( 𝐾𝑉𝑋𝑌𝑌𝐴 ) ∧ 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ) → ( 𝑌𝑦𝑋𝑦 ) )
6 5 ss2rabdv ( ( 𝐾𝑉𝑋𝑌𝑌𝐴 ) → { 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ∣ 𝑌𝑦 } ⊆ { 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ∣ 𝑋𝑦 } )
7 intss ( { 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ∣ 𝑌𝑦 } ⊆ { 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ∣ 𝑋𝑦 } → { 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ∣ 𝑋𝑦 } ⊆ { 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ∣ 𝑌𝑦 } )
8 6 7 syl ( ( 𝐾𝑉𝑋𝑌𝑌𝐴 ) → { 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ∣ 𝑋𝑦 } ⊆ { 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ∣ 𝑌𝑦 } )
9 simp1 ( ( 𝐾𝑉𝑋𝑌𝑌𝐴 ) → 𝐾𝑉 )
10 sstr ( ( 𝑋𝑌𝑌𝐴 ) → 𝑋𝐴 )
11 10 3adant1 ( ( 𝐾𝑉𝑋𝑌𝑌𝐴 ) → 𝑋𝐴 )
12 eqid ( PSubSp ‘ 𝐾 ) = ( PSubSp ‘ 𝐾 )
13 1 12 2 pclvalN ( ( 𝐾𝑉𝑋𝐴 ) → ( 𝑈𝑋 ) = { 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ∣ 𝑋𝑦 } )
14 9 11 13 syl2anc ( ( 𝐾𝑉𝑋𝑌𝑌𝐴 ) → ( 𝑈𝑋 ) = { 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ∣ 𝑋𝑦 } )
15 1 12 2 pclvalN ( ( 𝐾𝑉𝑌𝐴 ) → ( 𝑈𝑌 ) = { 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ∣ 𝑌𝑦 } )
16 15 3adant2 ( ( 𝐾𝑉𝑋𝑌𝑌𝐴 ) → ( 𝑈𝑌 ) = { 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ∣ 𝑌𝑦 } )
17 8 14 16 3sstr4d ( ( 𝐾𝑉𝑋𝑌𝑌𝐴 ) → ( 𝑈𝑋 ) ⊆ ( 𝑈𝑌 ) )