Proof of Theorem cdlema2N
| Step | Hyp | Ref
| Expression |
| 1 | | simp3ll 1245 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → 𝑅 ≠ 𝑃) |
| 2 | | simp3rl 1247 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → 𝑃 ≤ 𝑋) |
| 3 | | simp3rr 1248 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → ¬ 𝑄 ≤ 𝑋) |
| 4 | | simp3lr 1246 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → 𝑅 ≤ (𝑃 ∨ 𝑄)) |
| 5 | 2, 3, 4 | 3jca 1129 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) |
| 6 | | cdlema2.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
| 7 | | cdlema2.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
| 8 | | cdlema2.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
| 9 | | cdlema2.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
| 10 | 6, 7, 8, 9 | exatleN 39406 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ≤ 𝑋 ↔ 𝑅 = 𝑃)) |
| 11 | 5, 10 | syld3an3 1411 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → (𝑅 ≤ 𝑋 ↔ 𝑅 = 𝑃)) |
| 12 | 11 | necon3bbid 2978 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → (¬ 𝑅 ≤ 𝑋 ↔ 𝑅 ≠ 𝑃)) |
| 13 | 1, 12 | mpbird 257 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → ¬ 𝑅 ≤ 𝑋) |
| 14 | | simp1l 1198 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → 𝐾 ∈ HL) |
| 15 | | hlatl 39361 |
. . . 4
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
| 16 | 14, 15 | syl 17 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → 𝐾 ∈ AtLat) |
| 17 | | simp23 1209 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → 𝑅 ∈ 𝐴) |
| 18 | | simp1r 1199 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → 𝑋 ∈ 𝐵) |
| 19 | | cdlema2.m |
. . . 4
⊢ ∧ =
(meet‘𝐾) |
| 20 | | cdlema2.z |
. . . 4
⊢ 0 =
(0.‘𝐾) |
| 21 | 6, 7, 19, 20, 9 | atnle 39318 |
. . 3
⊢ ((𝐾 ∈ AtLat ∧ 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (¬ 𝑅 ≤ 𝑋 ↔ (𝑅 ∧ 𝑋) = 0 )) |
| 22 | 16, 17, 18, 21 | syl3anc 1373 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → (¬ 𝑅 ≤ 𝑋 ↔ (𝑅 ∧ 𝑋) = 0 )) |
| 23 | 13, 22 | mpbid 232 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → (𝑅 ∧ 𝑋) = 0 ) |