Theorem pclssidN

Description: A set of atoms is included in its projective subspace closure. (Contributed by NM, 12-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pclss.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	pclss.c	⊢ 𝑈 = ( PCl ‘ 𝐾 )
Assertion	pclssidN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → 𝑋 ⊆ ( 𝑈 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		pclss.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		pclss.c	⊢ 𝑈 = ( PCl ‘ 𝐾 )
3		ssintub	⊢ 𝑋 ⊆ ∩ { 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ∣ 𝑋 ⊆ 𝑦 }
4		eqid	⊢ ( PSubSp ‘ 𝐾 ) = ( PSubSp ‘ 𝐾 )
5	1 4 2	pclvalN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝑋 ) = ∩ { 𝑦 ∈ ( PSubSp ‘ 𝐾 ) ∣ 𝑋 ⊆ 𝑦 } )
6	3 5	sseqtrrid	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → 𝑋 ⊆ ( 𝑈 ‘ 𝑋 ) )