Proof of Theorem 4atexlemtlw
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. 2
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 2 | | 4thatlem0.l |
. 2
⊢ ≤ =
(le‘𝐾) |
| 3 | | 4thatlem.ph |
. . 3
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) |
| 4 | 3 | 4atexlemkl 40059 |
. 2
⊢ (𝜑 → 𝐾 ∈ Lat) |
| 5 | 3 | 4atexlemt 40055 |
. . 3
⊢ (𝜑 → 𝑇 ∈ 𝐴) |
| 6 | | 4thatlem0.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
| 7 | 1, 6 | atbase 39290 |
. . 3
⊢ (𝑇 ∈ 𝐴 → 𝑇 ∈ (Base‘𝐾)) |
| 8 | 5, 7 | syl 17 |
. 2
⊢ (𝜑 → 𝑇 ∈ (Base‘𝐾)) |
| 9 | 3 | 4atexlemk 40049 |
. . 3
⊢ (𝜑 → 𝐾 ∈ HL) |
| 10 | | 4thatlem0.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
| 11 | | 4thatlem0.m |
. . . 4
⊢ ∧ =
(meet‘𝐾) |
| 12 | | 4thatlem0.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
| 13 | | 4thatlem0.u |
. . . 4
⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) |
| 14 | 3, 2, 10, 11, 6, 12, 13 | 4atexlemu 40066 |
. . 3
⊢ (𝜑 → 𝑈 ∈ 𝐴) |
| 15 | | 4thatlem0.v |
. . . 4
⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊) |
| 16 | 3, 2, 10, 11, 6, 12, 13, 15 | 4atexlemv 40067 |
. . 3
⊢ (𝜑 → 𝑉 ∈ 𝐴) |
| 17 | 1, 10, 6 | hlatjcl 39368 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → (𝑈 ∨ 𝑉) ∈ (Base‘𝐾)) |
| 18 | 9, 14, 16, 17 | syl3anc 1373 |
. 2
⊢ (𝜑 → (𝑈 ∨ 𝑉) ∈ (Base‘𝐾)) |
| 19 | 3, 12 | 4atexlemwb 40061 |
. 2
⊢ (𝜑 → 𝑊 ∈ (Base‘𝐾)) |
| 20 | 3 | 4atexlemkc 40060 |
. . 3
⊢ (𝜑 → 𝐾 ∈ CvLat) |
| 21 | 3, 2, 10, 11, 6, 12, 13, 15 | 4atexlemunv 40068 |
. . 3
⊢ (𝜑 → 𝑈 ≠ 𝑉) |
| 22 | 3 | 4atexlemutvt 40056 |
. . 3
⊢ (𝜑 → (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇)) |
| 23 | 6, 2, 10 | cvlsupr4 39346 |
. . 3
⊢ ((𝐾 ∈ CvLat ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ≠ 𝑉 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) → 𝑇 ≤ (𝑈 ∨ 𝑉)) |
| 24 | 20, 14, 16, 5, 21, 22, 23 | syl132anc 1390 |
. 2
⊢ (𝜑 → 𝑇 ≤ (𝑈 ∨ 𝑉)) |
| 25 | 3 | 4atexlemp 40052 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
| 26 | 3 | 4atexlemq 40053 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
| 27 | 1, 10, 6 | hlatjcl 39368 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
| 28 | 9, 25, 26, 27 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
| 29 | 1, 2, 11 | latmle2 18510 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ≤ 𝑊) |
| 30 | 4, 28, 19, 29 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((𝑃 ∨ 𝑄) ∧ 𝑊) ≤ 𝑊) |
| 31 | 13, 30 | eqbrtrid 5178 |
. . 3
⊢ (𝜑 → 𝑈 ≤ 𝑊) |
| 32 | 3, 10, 6 | 4atexlempsb 40062 |
. . . . 5
⊢ (𝜑 → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) |
| 33 | 1, 2, 11 | latmle2 18510 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑆) ∧ 𝑊) ≤ 𝑊) |
| 34 | 4, 32, 19, 33 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((𝑃 ∨ 𝑆) ∧ 𝑊) ≤ 𝑊) |
| 35 | 15, 34 | eqbrtrid 5178 |
. . 3
⊢ (𝜑 → 𝑉 ≤ 𝑊) |
| 36 | 1, 6 | atbase 39290 |
. . . . 5
⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾)) |
| 37 | 14, 36 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾)) |
| 38 | 1, 6 | atbase 39290 |
. . . . 5
⊢ (𝑉 ∈ 𝐴 → 𝑉 ∈ (Base‘𝐾)) |
| 39 | 16, 38 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑉 ∈ (Base‘𝐾)) |
| 40 | 1, 2, 10 | latjle12 18495 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ 𝑉 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑈 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊) ↔ (𝑈 ∨ 𝑉) ≤ 𝑊)) |
| 41 | 4, 37, 39, 19, 40 | syl13anc 1374 |
. . 3
⊢ (𝜑 → ((𝑈 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊) ↔ (𝑈 ∨ 𝑉) ≤ 𝑊)) |
| 42 | 31, 35, 41 | mpbi2and 712 |
. 2
⊢ (𝜑 → (𝑈 ∨ 𝑉) ≤ 𝑊) |
| 43 | 1, 2, 4, 8, 18, 19, 24, 42 | lattrd 18491 |
1
⊢ (𝜑 → 𝑇 ≤ 𝑊) |