Metamath Proof Explorer

Theorem psubspi

Description: Property of a projective subspace. (Contributed by NM, 13-Jan-2012)

Ref Expression
Hypotheses psubspset.l ⊢ ≤ ˙ = ≤ K
psubspset.j ⊢ ∨ ˙ = join ⁡ K
psubspset.a ⊢ A = Atoms ⁡ K
psubspset.s ⊢ S = PSubSp ⁡ K
Assertion psubspi ⊢ K ∈ D ∧ X ∈ S ∧ P ∈ A ∧ ∃ q ∈ X ∃ r ∈ X P ≤ ˙ q ∨ ˙ r → P ∈ X

Proof

Step Hyp Ref Expression
1 psubspset.l ⊢ ≤ ˙ = ≤ K
2 psubspset.j ⊢ ∨ ˙ = join ⁡ K
3 psubspset.a ⊢ A = Atoms ⁡ K
4 psubspset.s ⊢ S = PSubSp ⁡ K
5 1 2 3 4 ispsubsp2 ⊢ K ∈ D → X ∈ S ↔ X ⊆ A ∧ ∀ p ∈ A ∃ q ∈ X ∃ r ∈ X p ≤ ˙ q ∨ ˙ r → p ∈ X
6 5 simplbda ⊢ K ∈ D ∧ X ∈ S → ∀ p ∈ A ∃ q ∈ X ∃ r ∈ X p ≤ ˙ q ∨ ˙ r → p ∈ X
7 6 ex ⊢ K ∈ D → X ∈ S → ∀ p ∈ A ∃ q ∈ X ∃ r ∈ X p ≤ ˙ q ∨ ˙ r → p ∈ X
8 breq1 ⊢ p = P → p ≤ ˙ q ∨ ˙ r ↔ P ≤ ˙ q ∨ ˙ r
9 8 2rexbidv ⊢ p = P → ∃ q ∈ X ∃ r ∈ X p ≤ ˙ q ∨ ˙ r ↔ ∃ q ∈ X ∃ r ∈ X P ≤ ˙ q ∨ ˙ r
10 eleq1 ⊢ p = P → p ∈ X ↔ P ∈ X
11 9 10 imbi12d ⊢ p = P → ∃ q ∈ X ∃ r ∈ X p ≤ ˙ q ∨ ˙ r → p ∈ X ↔ ∃ q ∈ X ∃ r ∈ X P ≤ ˙ q ∨ ˙ r → P ∈ X
12 11 rspccv ⊢ ∀ p ∈ A ∃ q ∈ X ∃ r ∈ X p ≤ ˙ q ∨ ˙ r → p ∈ X → P ∈ A → ∃ q ∈ X ∃ r ∈ X P ≤ ˙ q ∨ ˙ r → P ∈ X
13 7 12 syl6 ⊢ K ∈ D → X ∈ S → P ∈ A → ∃ q ∈ X ∃ r ∈ X P ≤ ˙ q ∨ ˙ r → P ∈ X
14 13 3imp1 ⊢ K ∈ D ∧ X ∈ S ∧ P ∈ A ∧ ∃ q ∈ X ∃ r ∈ X P ≤ ˙ q ∨ ˙ r → P ∈ X