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

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 ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝑋 ) ⊆ ( 𝑈 ‘ 𝑌 ) )