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

Metamath Proof Explorer

Theorem atnlej2

Description: If an atom is not less than or equal to the join of two others, it is not equal to either. (This also holds for non-atoms, but in this form it is convenient.) (Contributed by NM, 8-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 atnlej.l ⊢ ≤ ˙ = ≤ K
2 atnlej.j ⊢ ∨ ˙ = join ⁡ K
3 atnlej.a ⊢ A = Atoms ⁡ K
4 hllat ⊢ K ∈ HL → K ∈ Lat
5 4 3ad2ant1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ ¬ P ≤ ˙ Q ∨ ˙ R → K ∈ Lat
6 simp21 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ ¬ P ≤ ˙ Q ∨ ˙ R → P ∈ A
7 eqid ⊢ Base K = Base K
8 7 3 atbase ⊢ P ∈ A → P ∈ Base K
9 6 8 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ ¬ P ≤ ˙ Q ∨ ˙ R → P ∈ Base K
10 simp22 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ ¬ P ≤ ˙ Q ∨ ˙ R → Q ∈ A
11 7 3 atbase ⊢ Q ∈ A → Q ∈ Base K
12 10 11 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ ¬ P ≤ ˙ Q ∨ ˙ R → Q ∈ Base K
13 simp23 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ ¬ P ≤ ˙ Q ∨ ˙ R → R ∈ A
14 7 3 atbase ⊢ R ∈ A → R ∈ Base K
15 13 14 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ ¬ P ≤ ˙ Q ∨ ˙ R → R ∈ Base K
16 simp3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ ¬ P ≤ ˙ Q ∨ ˙ R → ¬ P ≤ ˙ Q ∨ ˙ R
17 7 1 2 latnlej1r ⊢ K ∈ Lat ∧ P ∈ Base K ∧ Q ∈ Base K ∧ R ∈ Base K ∧ ¬ P ≤ ˙ Q ∨ ˙ R → P ≠ R
18 5 9 12 15 16 17 syl131anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ ¬ P ≤ ˙ Q ∨ ˙ R → P ≠ R