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

Metamath Proof Explorer

Theorem cdlemg5

Description: TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle ? TODO: The .\/ hypothesis is unused. FIX COMMENT. (Contributed by NM, 26-Apr-2013)

Ref Expression
Hypotheses cdlemg5.l ⊢ ≤ ˙ = ≤ K
cdlemg5.j ⊢ ∨ ˙ = join ⁡ K
cdlemg5.a ⊢ A = Atoms ⁡ K
cdlemg5.h ⊢ H = LHyp ⁡ K
Assertion cdlemg5 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → ∃ q ∈ A P ≠ q ∧ ¬ q ≤ ˙ W

Proof

Step Hyp Ref Expression
1 cdlemg5.l ⊢ ≤ ˙ = ≤ K
2 cdlemg5.j ⊢ ∨ ˙ = join ⁡ K
3 cdlemg5.a ⊢ A = Atoms ⁡ K
4 cdlemg5.h ⊢ H = LHyp ⁡ K
5 1 3 4 lhpexle ⊢ K ∈ HL ∧ W ∈ H → ∃ r ∈ A r ≤ ˙ W
6 5 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → ∃ r ∈ A r ≤ ˙ W
7 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ r ∈ A ∧ r ≤ ˙ W → K ∈ HL ∧ W ∈ H
8 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ r ∈ A ∧ r ≤ ˙ W → r ∈ A ∧ r ≤ ˙ W
9 simplr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ r ∈ A ∧ r ≤ ˙ W → P ∈ A ∧ ¬ P ≤ ˙ W
10 1 2 3 4 cdlemf1 ⊢ K ∈ HL ∧ W ∈ H ∧ r ∈ A ∧ r ≤ ˙ W ∧ P ∈ A ∧ ¬ P ≤ ˙ W → ∃ q ∈ A P ≠ q ∧ ¬ q ≤ ˙ W ∧ r ≤ ˙ P ∨ ˙ q
11 7 8 9 10 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ r ∈ A ∧ r ≤ ˙ W → ∃ q ∈ A P ≠ q ∧ ¬ q ≤ ˙ W ∧ r ≤ ˙ P ∨ ˙ q
12 3simpa ⊢ P ≠ q ∧ ¬ q ≤ ˙ W ∧ r ≤ ˙ P ∨ ˙ q → P ≠ q ∧ ¬ q ≤ ˙ W
13 12 reximi ⊢ ∃ q ∈ A P ≠ q ∧ ¬ q ≤ ˙ W ∧ r ≤ ˙ P ∨ ˙ q → ∃ q ∈ A P ≠ q ∧ ¬ q ≤ ˙ W
14 11 13 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ r ∈ A ∧ r ≤ ˙ W → ∃ q ∈ A P ≠ q ∧ ¬ q ≤ ˙ W
15 6 14 rexlimddv ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → ∃ q ∈ A P ≠ q ∧ ¬ q ≤ ˙ W