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

Metamath Proof Explorer

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	$⊢ A = Atoms (K)$
	atpsub.s	$⊢ S = PSubSp (K)$
Assertion	psubatN	$⊢ (K \in B \land X \in S \land Y \in X) \to Y \in A$

Step	Hyp	Ref	Expression
1		atpsub.a	$⊢ A = Atoms (K)$
2		atpsub.s	$⊢ S = PSubSp (K)$
3	1 2	psubssat	$⊢ (K \in B \land X \in S) \to X \subseteq A$
4	3	sseld	$⊢ (K \in B \land X \in S) \to (Y \in X \to Y \in A)$
5	4	3impia	$⊢ (K \in B \land X \in S \land Y \in X) \to Y \in A$