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