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

Metamath Proof Explorer

Theorem hlatcon2

Description: Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012)

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

Proof

Step Hyp Ref Expression
1 3noncol.l ⊢ ≤ ˙ = ≤ K
2 3noncol.j ⊢ ∨ ˙ = join ⁡ K
3 3noncol.a ⊢ A = Atoms ⁡ K
4 1 2 3 hlatcon3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → ¬ P ≤ ˙ Q ∨ ˙ R
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 2 3 hlatjcom ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A → Q ∨ ˙ R = R ∨ ˙ Q
9 5 6 7 8 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → Q ∨ ˙ R = R ∨ ˙ Q
10 9 breq2d ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → P ≤ ˙ Q ∨ ˙ R ↔ P ≤ ˙ R ∨ ˙ Q
11 4 10 mtbid ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → ¬ P ≤ ˙ R ∨ ˙ Q