Description: Lemma for 4atexlem7 . (Contributed by NM, 23-Nov-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | 4thatlem.ph | ⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) | |
| 4thatlemslps.l | ⊢ ≤ = ( le ‘ 𝐾 ) | ||
| 4thatlemslps.j | ⊢ ∨ = ( join ‘ 𝐾 ) | ||
| 4thatlemslps.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | ||
| Assertion | 4atexlempns | ⊢ ( 𝜑 → 𝑃 ≠ 𝑆 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 4thatlem.ph | ⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) | |
| 2 | 4thatlemslps.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
| 3 | 4thatlemslps.j | ⊢ ∨ = ( join ‘ 𝐾 ) | |
| 4 | 4thatlemslps.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | |
| 5 | 1 | 4atexlemk | ⊢ ( 𝜑 → 𝐾 ∈ HL ) |
| 6 | 1 | 4atexlemp | ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 ) |
| 7 | 1 | 4atexlemq | ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 ) |
| 8 | 1 | 4atexlems | ⊢ ( 𝜑 → 𝑆 ∈ 𝐴 ) |
| 9 | 1 | 4atexlemnslpq | ⊢ ( 𝜑 → ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) |
| 10 | 2 3 4 | 4atlem0be | ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑃 ≠ 𝑆 ) |
| 11 | 5 6 7 8 9 10 | syl131anc | ⊢ ( 𝜑 → 𝑃 ≠ 𝑆 ) |