Theorem psubatN

Description: A member of a projective subspace is an atom. (Contributed by NM, 4-Nov-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	atpsub.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	atpsub.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
Assertion	psubatN	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑋 ) → 𝑌 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		atpsub.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		atpsub.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
3	1 2	psubssat	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ⊆ 𝐴 )
4	3	sseld	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑌 ∈ 𝑋 → 𝑌 ∈ 𝐴 ) )
5	4	3impia	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑋 ) → 𝑌 ∈ 𝐴 )