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

Metamath Proof Explorer

Theorem lhpexle2

Description: There exists atom under a co-atom different from any two other elements. (Contributed by NM, 24-Jul-2013)

Ref Expression
Hypotheses lhpex1.l ⊢ ≤ ˙ = ≤ K
lhpex1.a ⊢ A = Atoms ⁡ K
lhpex1.h ⊢ H = LHyp ⁡ K
Assertion lhpexle2 ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ A p ≤ ˙ W ∧ p ≠ X ∧ p ≠ Y

Proof

Step Hyp Ref Expression
1 lhpex1.l ⊢ ≤ ˙ = ≤ K
2 lhpex1.a ⊢ A = Atoms ⁡ K
3 lhpex1.h ⊢ H = LHyp ⁡ K
4 1 2 3 lhpexle1 ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ A p ≤ ˙ W ∧ p ≠ X
5 1 2 3 lhpexle1 ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ A p ≤ ˙ W ∧ p ≠ Y
6 5 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ A ∧ Y ≤ ˙ W → ∃ p ∈ A p ≤ ˙ W ∧ p ≠ Y
7 1 2 3 lhpexle2lem ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ A ∧ Y ≤ ˙ W ∧ X ∈ A ∧ X ≤ ˙ W → ∃ p ∈ A p ≤ ˙ W ∧ p ≠ Y ∧ p ≠ X
8 7 3expa ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ A ∧ Y ≤ ˙ W ∧ X ∈ A ∧ X ≤ ˙ W → ∃ p ∈ A p ≤ ˙ W ∧ p ≠ Y ∧ p ≠ X
9 6 8 lhpexle1lem ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ A ∧ Y ≤ ˙ W → ∃ p ∈ A p ≤ ˙ W ∧ p ≠ Y ∧ p ≠ X
10 3ancomb ⊢ p ≤ ˙ W ∧ p ≠ Y ∧ p ≠ X ↔ p ≤ ˙ W ∧ p ≠ X ∧ p ≠ Y
11 10 rexbii ⊢ ∃ p ∈ A p ≤ ˙ W ∧ p ≠ Y ∧ p ≠ X ↔ ∃ p ∈ A p ≤ ˙ W ∧ p ≠ X ∧ p ≠ Y
12 9 11 sylib ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ A ∧ Y ≤ ˙ W → ∃ p ∈ A p ≤ ˙ W ∧ p ≠ X ∧ p ≠ Y
13 4 12 lhpexle1lem ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ A p ≤ ˙ W ∧ p ≠ X ∧ p ≠ Y