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

Metamath Proof Explorer

Theorem psubssat

Description: A projective subspace consists of atoms. (Contributed by NM, 4-Nov-2011)

Ref Expression
Hypotheses atpsub.a ⊢ A = Atoms ⁡ K
atpsub.s ⊢ S = PSubSp ⁡ K
Assertion psubssat ⊢ K ∈ B ∧ X ∈ S → X ⊆ A

Proof

Step Hyp Ref Expression
1 atpsub.a ⊢ A = Atoms ⁡ K
2 atpsub.s ⊢ S = PSubSp ⁡ K
3 eqid ⊢ ≤ K = ≤ K
4 eqid ⊢ join ⁡ K = join ⁡ K
5 3 4 1 2 ispsubsp ⊢ K ∈ B → X ∈ S ↔ X ⊆ A ∧ ∀ p ∈ X ∀ q ∈ X ∀ r ∈ A r ≤ K p join ⁡ K q → r ∈ X
6 5 simprbda ⊢ K ∈ B ∧ X ∈ S → X ⊆ A