Proof of Theorem 4atexlemex2
Step | Hyp | Ref
| Expression |
1 | | 4thatlem.ph |
. . . 4
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) |
2 | | 4thatlem0.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
3 | | 4thatlem0.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
4 | | 4thatlem0.m |
. . . 4
⊢ ∧ =
(meet‘𝐾) |
5 | | 4thatlem0.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
6 | | 4thatlem0.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
7 | | 4thatlem0.u |
. . . 4
⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) |
8 | | 4thatlem0.v |
. . . 4
⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊) |
9 | | 4thatlem0.c |
. . . 4
⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | 4atexlemc 36137 |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝐴) |
11 | 10 | adantr 474 |
. 2
⊢ ((𝜑 ∧ 𝐶 ≠ 𝑆) → 𝐶 ∈ 𝐴) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | 4atexlemnclw 36138 |
. . 3
⊢ (𝜑 → ¬ 𝐶 ≤ 𝑊) |
13 | 12 | adantr 474 |
. 2
⊢ ((𝜑 ∧ 𝐶 ≠ 𝑆) → ¬ 𝐶 ≤ 𝑊) |
14 | 1, 2, 3, 4, 5, 6, 7, 8 | 4atexlemntlpq 36136 |
. . . . 5
⊢ (𝜑 → ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) |
15 | | id 22 |
. . . . . . . . . . 11
⊢ (𝐶 = 𝑃 → 𝐶 = 𝑃) |
16 | 9, 15 | syl5eqr 2875 |
. . . . . . . . . 10
⊢ (𝐶 = 𝑃 → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) = 𝑃) |
17 | 16 | adantl 475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 = 𝑃) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) = 𝑃) |
18 | 1 | 4atexlemkl 36125 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ Lat) |
19 | 1, 3, 5 | 4atexlemqtb 36129 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 ∨ 𝑇) ∈ (Base‘𝐾)) |
20 | 1, 3, 5 | 4atexlempsb 36128 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) |
21 | | eqid 2825 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐾) =
(Base‘𝐾) |
22 | 21, 2, 4 | latmle1 17429 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑄 ∨ 𝑇)) |
23 | 18, 19, 20, 22 | syl3anc 1494 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑄 ∨ 𝑇)) |
24 | 1 | 4atexlemk 36115 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ HL) |
25 | 1 | 4atexlemq 36119 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
26 | 1 | 4atexlemt 36121 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ 𝐴) |
27 | 3, 5 | hlatjcom 35436 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑄 ∨ 𝑇) = (𝑇 ∨ 𝑄)) |
28 | 24, 25, 26, 27 | syl3anc 1494 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄 ∨ 𝑇) = (𝑇 ∨ 𝑄)) |
29 | 23, 28 | breqtrd 4899 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑇 ∨ 𝑄)) |
30 | 29 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 = 𝑃) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑇 ∨ 𝑄)) |
31 | 17, 30 | eqbrtrrd 4897 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 = 𝑃) → 𝑃 ≤ (𝑇 ∨ 𝑄)) |
32 | 1 | 4atexlemkc 36126 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ CvLat) |
33 | 1 | 4atexlemp 36118 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
34 | 1 | 4atexlempnq 36123 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ≠ 𝑄) |
35 | 2, 3, 5 | cvlatexch2 35405 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑃 ≤ (𝑇 ∨ 𝑄) → 𝑇 ≤ (𝑃 ∨ 𝑄))) |
36 | 32, 33, 26, 25, 34, 35 | syl131anc 1506 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 ≤ (𝑇 ∨ 𝑄) → 𝑇 ≤ (𝑃 ∨ 𝑄))) |
37 | 36 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 = 𝑃) → (𝑃 ≤ (𝑇 ∨ 𝑄) → 𝑇 ≤ (𝑃 ∨ 𝑄))) |
38 | 31, 37 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 = 𝑃) → 𝑇 ≤ (𝑃 ∨ 𝑄)) |
39 | 38 | ex 403 |
. . . . . 6
⊢ (𝜑 → (𝐶 = 𝑃 → 𝑇 ≤ (𝑃 ∨ 𝑄))) |
40 | 39 | necon3bd 3013 |
. . . . 5
⊢ (𝜑 → (¬ 𝑇 ≤ (𝑃 ∨ 𝑄) → 𝐶 ≠ 𝑃)) |
41 | 14, 40 | mpd 15 |
. . . 4
⊢ (𝜑 → 𝐶 ≠ 𝑃) |
42 | 41 | adantr 474 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ≠ 𝑆) → 𝐶 ≠ 𝑃) |
43 | | simpr 479 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ≠ 𝑆) → 𝐶 ≠ 𝑆) |
44 | 21, 2, 4 | latmle2 17430 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑃 ∨ 𝑆)) |
45 | 18, 19, 20, 44 | syl3anc 1494 |
. . . . 5
⊢ (𝜑 → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑃 ∨ 𝑆)) |
46 | 9, 45 | syl5eqbr 4908 |
. . . 4
⊢ (𝜑 → 𝐶 ≤ (𝑃 ∨ 𝑆)) |
47 | 46 | adantr 474 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ≠ 𝑆) → 𝐶 ≤ (𝑃 ∨ 𝑆)) |
48 | 1 | 4atexlems 36120 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ 𝐴) |
49 | 1, 2, 3, 5 | 4atexlempns 36130 |
. . . . 5
⊢ (𝜑 → 𝑃 ≠ 𝑆) |
50 | 5, 2, 3 | cvlsupr2 35411 |
. . . . 5
⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) ∧ 𝑃 ≠ 𝑆) → ((𝑃 ∨ 𝐶) = (𝑆 ∨ 𝐶) ↔ (𝐶 ≠ 𝑃 ∧ 𝐶 ≠ 𝑆 ∧ 𝐶 ≤ (𝑃 ∨ 𝑆)))) |
51 | 32, 33, 48, 10, 49, 50 | syl131anc 1506 |
. . . 4
⊢ (𝜑 → ((𝑃 ∨ 𝐶) = (𝑆 ∨ 𝐶) ↔ (𝐶 ≠ 𝑃 ∧ 𝐶 ≠ 𝑆 ∧ 𝐶 ≤ (𝑃 ∨ 𝑆)))) |
52 | 51 | adantr 474 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ≠ 𝑆) → ((𝑃 ∨ 𝐶) = (𝑆 ∨ 𝐶) ↔ (𝐶 ≠ 𝑃 ∧ 𝐶 ≠ 𝑆 ∧ 𝐶 ≤ (𝑃 ∨ 𝑆)))) |
53 | 42, 43, 47, 52 | mpbir3and 1446 |
. 2
⊢ ((𝜑 ∧ 𝐶 ≠ 𝑆) → (𝑃 ∨ 𝐶) = (𝑆 ∨ 𝐶)) |
54 | | breq1 4876 |
. . . . 5
⊢ (𝑧 = 𝐶 → (𝑧 ≤ 𝑊 ↔ 𝐶 ≤ 𝑊)) |
55 | 54 | notbid 310 |
. . . 4
⊢ (𝑧 = 𝐶 → (¬ 𝑧 ≤ 𝑊 ↔ ¬ 𝐶 ≤ 𝑊)) |
56 | | oveq2 6913 |
. . . . 5
⊢ (𝑧 = 𝐶 → (𝑃 ∨ 𝑧) = (𝑃 ∨ 𝐶)) |
57 | | oveq2 6913 |
. . . . 5
⊢ (𝑧 = 𝐶 → (𝑆 ∨ 𝑧) = (𝑆 ∨ 𝐶)) |
58 | 56, 57 | eqeq12d 2840 |
. . . 4
⊢ (𝑧 = 𝐶 → ((𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧) ↔ (𝑃 ∨ 𝐶) = (𝑆 ∨ 𝐶))) |
59 | 55, 58 | anbi12d 624 |
. . 3
⊢ (𝑧 = 𝐶 → ((¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧)) ↔ (¬ 𝐶 ≤ 𝑊 ∧ (𝑃 ∨ 𝐶) = (𝑆 ∨ 𝐶)))) |
60 | 59 | rspcev 3526 |
. 2
⊢ ((𝐶 ∈ 𝐴 ∧ (¬ 𝐶 ≤ 𝑊 ∧ (𝑃 ∨ 𝐶) = (𝑆 ∨ 𝐶))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧))) |
61 | 11, 13, 53, 60 | syl12anc 870 |
1
⊢ ((𝜑 ∧ 𝐶 ≠ 𝑆) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧))) |