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

Metamath Proof Explorer

Theorem 2llnne2N

Description: Condition implying that two intersecting lines are different. (Contributed by NM, 13-Jun-2012) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 2lnne.l ⊢ ≤ ˙ = ≤ K
2 2lnne.j ⊢ ∨ ˙ = join ⁡ K
3 2lnne.a ⊢ A = Atoms ⁡ K
4 simpl ⊢ K ∈ HL ∧ P ∈ A ∧ R ∈ A → K ∈ HL
5 simprr ⊢ K ∈ HL ∧ P ∈ A ∧ R ∈ A → R ∈ A
6 simprl ⊢ K ∈ HL ∧ P ∈ A ∧ R ∈ A → P ∈ A
7 1 2 3 hlatlej2 ⊢ K ∈ HL ∧ R ∈ A ∧ P ∈ A → P ≤ ˙ R ∨ ˙ P
8 4 5 6 7 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ R ∈ A → P ≤ ˙ R ∨ ˙ P
9 breq2 ⊢ R ∨ ˙ P = R ∨ ˙ Q → P ≤ ˙ R ∨ ˙ P ↔ P ≤ ˙ R ∨ ˙ Q
10 8 9 syl5ibcom ⊢ K ∈ HL ∧ P ∈ A ∧ R ∈ A → R ∨ ˙ P = R ∨ ˙ Q → P ≤ ˙ R ∨ ˙ Q
11 10 necon3bd ⊢ K ∈ HL ∧ P ∈ A ∧ R ∈ A → ¬ P ≤ ˙ R ∨ ˙ Q → R ∨ ˙ P ≠ R ∨ ˙ Q
12 11 3impia ⊢ K ∈ HL ∧ P ∈ A ∧ R ∈ A ∧ ¬ P ≤ ˙ R ∨ ˙ Q → R ∨ ˙ P ≠ R ∨ ˙ Q