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

Metamath Proof Explorer

Theorem 4atlem0ae

Description: Lemma for 4at . (Contributed by NM, 10-Jul-2012)

Ref Expression
Hypotheses 4at.l ⊢ ≤ ˙ = ≤ K
4at.j ⊢ ∨ ˙ = join ⁡ K
4at.a ⊢ A = Atoms ⁡ K
Assertion 4atlem0ae ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → ¬ Q ≤ ˙ P ∨ ˙ R

Proof

Step Hyp Ref Expression
1 4at.l ⊢ ≤ ˙ = ≤ K
2 4at.j ⊢ ∨ ˙ = join ⁡ K
3 4at.a ⊢ A = Atoms ⁡ K
4 simp3r ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → ¬ R ≤ ˙ P ∨ ˙ Q
5 simp1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → K ∈ HL
6 simp22 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → Q ∈ A
7 simp23 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → R ∈ A
8 simp21 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → P ∈ A
9 simp3l ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → P ≠ Q
10 9 necomd ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → Q ≠ P
11 1 2 3 hlatexch1 ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A ∧ P ∈ A ∧ Q ≠ P → Q ≤ ˙ P ∨ ˙ R → R ≤ ˙ P ∨ ˙ Q
12 5 6 7 8 10 11 syl131anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → Q ≤ ˙ P ∨ ˙ R → R ≤ ˙ P ∨ ˙ Q
13 4 12 mtod ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → ¬ Q ≤ ˙ P ∨ ˙ R