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

Metamath Proof Explorer

Theorem lhpocnel2

Description: The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 20-Feb-2014)

Ref Expression
Hypotheses lhpocnel2.l ⊢ ≤ ˙ = ≤ K
lhpocnel2.a ⊢ A = Atoms ⁡ K
lhpocnel2.h ⊢ H = LHyp ⁡ K
lhpocnel2.p ⊢ P = oc ⁡ K ⁡ W
Assertion lhpocnel2 ⊢ K ∈ HL ∧ W ∈ H → P ∈ A ∧ ¬ P ≤ ˙ W

Proof

Step Hyp Ref Expression
1 lhpocnel2.l ⊢ ≤ ˙ = ≤ K
2 lhpocnel2.a ⊢ A = Atoms ⁡ K
3 lhpocnel2.h ⊢ H = LHyp ⁡ K
4 lhpocnel2.p ⊢ P = oc ⁡ K ⁡ W
5 eqid ⊢ oc ⁡ K = oc ⁡ K
6 1 5 2 3 lhpocnel ⊢ K ∈ HL ∧ W ∈ H → oc ⁡ K ⁡ W ∈ A ∧ ¬ oc ⁡ K ⁡ W ≤ ˙ W
7 4 eleq1i ⊢ P ∈ A ↔ oc ⁡ K ⁡ W ∈ A
8 4 breq1i ⊢ P ≤ ˙ W ↔ oc ⁡ K ⁡ W ≤ ˙ W
9 8 notbii ⊢ ¬ P ≤ ˙ W ↔ ¬ oc ⁡ K ⁡ W ≤ ˙ W
10 7 9 anbi12i ⊢ P ∈ A ∧ ¬ P ≤ ˙ W ↔ oc ⁡ K ⁡ W ∈ A ∧ ¬ oc ⁡ K ⁡ W ≤ ˙ W
11 6 10 sylibr ⊢ K ∈ HL ∧ W ∈ H → P ∈ A ∧ ¬ P ≤ ˙ W