Description: Part of proof of Lemma E in Crawley p. 113. See cdleme3 . (Contributed by NM, 6-Oct-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cdleme1.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
| cdleme1.j | ⊢ ∨ = ( join ‘ 𝐾 ) | ||
| cdleme1.m | ⊢ ∧ = ( meet ‘ 𝐾 ) | ||
| cdleme1.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | ||
| cdleme1.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | ||
| cdleme1.u | ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) | ||
| cdleme1.f | ⊢ 𝐹 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) | ||
| Assertion | cdleme3fa | ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐹 ∈ 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cdleme1.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
| 2 | cdleme1.j | ⊢ ∨ = ( join ‘ 𝐾 ) | |
| 3 | cdleme1.m | ⊢ ∧ = ( meet ‘ 𝐾 ) | |
| 4 | cdleme1.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | |
| 5 | cdleme1.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
| 6 | cdleme1.u | ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) | |
| 7 | cdleme1.f | ⊢ 𝐹 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) | |
| 8 | eqid | ⊢ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) | |
| 9 | 1 2 3 4 5 6 7 8 | cdleme3h | ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐹 ∈ 𝐴 ) |