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

Metamath Proof Explorer

Theorem 1dimN

Description: An atom is covered by a height-2 element (1-dimensional line). (Contributed by NM, 3-May-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2dim.j ⊢ ∨ ˙ = join ⁡ K
2dim.c ⊢ C = ⋖ K
2dim.a ⊢ A = Atoms ⁡ K
Assertion 1dimN ⊢ K ∈ HL ∧ P ∈ A → ∃ q ∈ A P C P ∨ ˙ q

Proof

Step Hyp Ref Expression
1 2dim.j ⊢ ∨ ˙ = join ⁡ K
2 2dim.c ⊢ C = ⋖ K
3 2dim.a ⊢ A = Atoms ⁡ K
4 1 2 3 2dim ⊢ K ∈ HL ∧ P ∈ A → ∃ q ∈ A ∃ r ∈ A P C P ∨ ˙ q ∧ P ∨ ˙ q C P ∨ ˙ q ∨ ˙ r
5 r19.42v ⊢ ∃ r ∈ A P C P ∨ ˙ q ∧ P ∨ ˙ q C P ∨ ˙ q ∨ ˙ r ↔ P C P ∨ ˙ q ∧ ∃ r ∈ A P ∨ ˙ q C P ∨ ˙ q ∨ ˙ r
6 5 simplbi ⊢ ∃ r ∈ A P C P ∨ ˙ q ∧ P ∨ ˙ q C P ∨ ˙ q ∨ ˙ r → P C P ∨ ˙ q
7 6 reximi ⊢ ∃ q ∈ A ∃ r ∈ A P C P ∨ ˙ q ∧ P ∨ ˙ q C P ∨ ˙ q ∨ ˙ r → ∃ q ∈ A P C P ∨ ˙ q
8 4 7 syl ⊢ K ∈ HL ∧ P ∈ A → ∃ q ∈ A P C P ∨ ˙ q