Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cdlemesner.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
| cdlemesner.j | ⊢ ∨ = ( join ‘ 𝐾 ) | ||
| cdlemesner.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | ||
| cdlemesner.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | ||
| Assertion | cdlemesner | ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑆 ≠ 𝑅 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cdlemesner.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
| 2 | cdlemesner.j | ⊢ ∨ = ( join ‘ 𝐾 ) | |
| 3 | cdlemesner.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | |
| 4 | cdlemesner.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
| 5 | nbrne2 | ⊢ ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑅 ≠ 𝑆 ) | |
| 6 | 5 | 3ad2ant3 | ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑅 ≠ 𝑆 ) |
| 7 | 6 | necomd | ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑆 ≠ 𝑅 ) |