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

Metamath Proof Explorer

Theorem atpsubN

Description: The set of all atoms is a projective subspace. Remark below Definition 15.1 of MaedaMaeda p. 61. (Contributed by NM, 13-Oct-2011) (New usage is discouraged.)

Ref Expression
Hypotheses atpsub.a ⊢ A = Atoms ⁡ K
atpsub.s ⊢ S = PSubSp ⁡ K
Assertion atpsubN ⊢ K ∈ V → A ∈ S

Proof

Step Hyp Ref Expression
1 atpsub.a ⊢ A = Atoms ⁡ K
2 atpsub.s ⊢ S = PSubSp ⁡ K
3 ssid ⊢ A ⊆ A
4 ax-1 ⊢ r ∈ A → r ≤ K p join ⁡ K q → r ∈ A
5 4 rgen ⊢ ∀ r ∈ A r ≤ K p join ⁡ K q → r ∈ A
6 5 rgen2w ⊢ ∀ p ∈ A ∀ q ∈ A ∀ r ∈ A r ≤ K p join ⁡ K q → r ∈ A
7 3 6 pm3.2i ⊢ A ⊆ A ∧ ∀ p ∈ A ∀ q ∈ A ∀ r ∈ A r ≤ K p join ⁡ K q → r ∈ A
8 eqid ⊢ ≤ K = ≤ K
9 eqid ⊢ join ⁡ K = join ⁡ K
10 8 9 1 2 ispsubsp ⊢ K ∈ V → A ∈ S ↔ A ⊆ A ∧ ∀ p ∈ A ∀ q ∈ A ∀ r ∈ A r ≤ K p join ⁡ K q → r ∈ A
11 7 10 mpbiri ⊢ K ∈ V → A ∈ S