Metamath Proof Explorer

Theorem 0psubN

Description: The empty set 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
Hypothesis 0psub.s ⊢ S = PSubSp ⁡ K
Assertion 0psubN ⊢ K ∈ V → ∅ ∈ S

Proof

Step Hyp Ref Expression
1 0psub.s ⊢ S = PSubSp ⁡ K
2 0ss ⊢ ∅ ⊆ Atoms ⁡ K
3 ral0 ⊢ ∀ p ∈ ∅ ∀ q ∈ ∅ ∀ r ∈ Atoms ⁡ K r ≤ K p join ⁡ K q → r ∈ ∅
4 2 3 pm3.2i ⊢ ∅ ⊆ Atoms ⁡ K ∧ ∀ p ∈ ∅ ∀ q ∈ ∅ ∀ r ∈ Atoms ⁡ K r ≤ K p join ⁡ K q → r ∈ ∅
5 eqid ⊢ ≤ K = ≤ K
6 eqid ⊢ join ⁡ K = join ⁡ K
7 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
8 5 6 7 1 ispsubsp ⊢ K ∈ V → ∅ ∈ S ↔ ∅ ⊆ Atoms ⁡ K ∧ ∀ p ∈ ∅ ∀ q ∈ ∅ ∀ r ∈ Atoms ⁡ K r ≤ K p join ⁡ K q → r ∈ ∅
9 4 8 mpbiri ⊢ K ∈ V → ∅ ∈ S