Step | Hyp | Ref
| Expression |
1 | | hllat 33668 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
2 | | cvrexch.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐾) |
3 | | cvrexch.m |
. . . . . . . 8
⊢ ∧ =
(meet‘𝐾) |
4 | 2, 3 | latmcl 16875 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵) |
5 | 1, 4 | syl3an1 1351 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵) |
6 | | eqid 2610 |
. . . . . . . 8
⊢
(lt‘𝐾) =
(lt‘𝐾) |
7 | | cvrexch.c |
. . . . . . . 8
⊢ 𝐶 = ( ⋖ ‘𝐾) |
8 | 2, 6, 7 | cvrlt 33575 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌)𝐶𝑌) → (𝑋 ∧ 𝑌)(lt‘𝐾)𝑌) |
9 | 8 | ex 449 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 → (𝑋 ∧ 𝑌)(lt‘𝐾)𝑌)) |
10 | 5, 9 | syld3an2 1365 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 → (𝑋 ∧ 𝑌)(lt‘𝐾)𝑌)) |
11 | | eqid 2610 |
. . . . . . 7
⊢
(le‘𝐾) =
(le‘𝐾) |
12 | | eqid 2610 |
. . . . . . 7
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
13 | 2, 11, 6, 12 | hlrelat1 33704 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)(lt‘𝐾)𝑌 → ∃𝑝 ∈ (Atoms‘𝐾)(¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌))) |
14 | 5, 13 | syld3an2 1365 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)(lt‘𝐾)𝑌 → ∃𝑝 ∈ (Atoms‘𝐾)(¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌))) |
15 | 10, 14 | syld 46 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 → ∃𝑝 ∈ (Atoms‘𝐾)(¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌))) |
16 | 15 | imp 444 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌)𝐶𝑌) → ∃𝑝 ∈ (Atoms‘𝐾)(¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌)) |
17 | | simpl1 1057 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → 𝐾 ∈ HL) |
18 | 17, 1 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → 𝐾 ∈ Lat) |
19 | 2, 12 | atbase 33594 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ (Atoms‘𝐾) → 𝑝 ∈ 𝐵) |
20 | 19 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → 𝑝 ∈ 𝐵) |
21 | | simpl2 1058 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → 𝑋 ∈ 𝐵) |
22 | | simpl3 1059 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → 𝑌 ∈ 𝐵) |
23 | 2, 11, 3 | latlem12 16901 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ Lat ∧ (𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑝(le‘𝐾)𝑋 ∧ 𝑝(le‘𝐾)𝑌) ↔ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌))) |
24 | 18, 20, 21, 22, 23 | syl13anc 1320 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → ((𝑝(le‘𝐾)𝑋 ∧ 𝑝(le‘𝐾)𝑌) ↔ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌))) |
25 | 24 | biimpd 218 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → ((𝑝(le‘𝐾)𝑋 ∧ 𝑝(le‘𝐾)𝑌) → 𝑝(le‘𝐾)(𝑋 ∧ 𝑌))) |
26 | 25 | expcomd 453 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → (𝑝(le‘𝐾)𝑌 → (𝑝(le‘𝐾)𝑋 → 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)))) |
27 | | con3 148 |
. . . . . . . . . . . . 13
⊢ ((𝑝(le‘𝐾)𝑋 → 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) → ¬ 𝑝(le‘𝐾)𝑋)) |
28 | 26, 27 | syl6 34 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → (𝑝(le‘𝐾)𝑌 → (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) → ¬ 𝑝(le‘𝐾)𝑋))) |
29 | 28 | com23 84 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) → (𝑝(le‘𝐾)𝑌 → ¬ 𝑝(le‘𝐾)𝑋))) |
30 | 29 | a1d 25 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → ((𝑋 ∧ 𝑌)𝐶𝑌 → (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) → (𝑝(le‘𝐾)𝑌 → ¬ 𝑝(le‘𝐾)𝑋)))) |
31 | 30 | imp4d 616 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → (((𝑋 ∧ 𝑌)𝐶𝑌 ∧ (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌)) → ¬ 𝑝(le‘𝐾)𝑋)) |
32 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → 𝑝 ∈ (Atoms‘𝐾)) |
33 | | cvrexch.j |
. . . . . . . . . . 11
⊢ ∨ =
(join‘𝐾) |
34 | 2, 11, 33, 7, 12 | cvr1 33714 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑝 ∈ (Atoms‘𝐾)) → (¬ 𝑝(le‘𝐾)𝑋 ↔ 𝑋𝐶(𝑋 ∨ 𝑝))) |
35 | 17, 21, 32, 34 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → (¬ 𝑝(le‘𝐾)𝑋 ↔ 𝑋𝐶(𝑋 ∨ 𝑝))) |
36 | 31, 35 | sylibd 228 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) → (((𝑋 ∧ 𝑌)𝐶𝑌 ∧ (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌)) → 𝑋𝐶(𝑋 ∨ 𝑝))) |
37 | 36 | imp 444 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) ∧ ((𝑋 ∧ 𝑌)𝐶𝑌 ∧ (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌))) → 𝑋𝐶(𝑋 ∨ 𝑝)) |
38 | | simpl1 1057 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → 𝐾 ∈ HL) |
39 | 38, 1 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → 𝐾 ∈ Lat) |
40 | | simpl2 1058 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
41 | | simpl3 1059 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → 𝑌 ∈ 𝐵) |
42 | 39, 40, 41, 4 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵) |
43 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → 𝑝 ∈ 𝐵) |
44 | 2, 33 | latjass 16918 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑝 ∈ 𝐵)) → ((𝑋 ∨ (𝑋 ∧ 𝑌)) ∨ 𝑝) = (𝑋 ∨ ((𝑋 ∧ 𝑌) ∨ 𝑝))) |
45 | 39, 40, 42, 43, 44 | syl13anc 1320 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → ((𝑋 ∨ (𝑋 ∧ 𝑌)) ∨ 𝑝) = (𝑋 ∨ ((𝑋 ∧ 𝑌) ∨ 𝑝))) |
46 | 2, 33, 3 | latabs1 16910 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ (𝑋 ∧ 𝑌)) = 𝑋) |
47 | 1, 46 | syl3an1 1351 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ (𝑋 ∧ 𝑌)) = 𝑋) |
48 | 47 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → (𝑋 ∨ (𝑋 ∧ 𝑌)) = 𝑋) |
49 | 48 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → ((𝑋 ∨ (𝑋 ∧ 𝑌)) ∨ 𝑝) = (𝑋 ∨ 𝑝)) |
50 | 45, 49 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → (𝑋 ∨ ((𝑋 ∧ 𝑌) ∨ 𝑝)) = (𝑋 ∨ 𝑝)) |
51 | 50 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) ∧ ((𝑋 ∧ 𝑌)𝐶𝑌 ∧ (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌))) → (𝑋 ∨ ((𝑋 ∧ 𝑌) ∨ 𝑝)) = (𝑋 ∨ 𝑝)) |
52 | 2, 11, 6, 33 | latnle 16908 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑝 ∈ 𝐵) → (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ↔ (𝑋 ∧ 𝑌)(lt‘𝐾)((𝑋 ∧ 𝑌) ∨ 𝑝))) |
53 | 39, 42, 43, 52 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ↔ (𝑋 ∧ 𝑌)(lt‘𝐾)((𝑋 ∧ 𝑌) ∨ 𝑝))) |
54 | 2, 11, 3 | latmle2 16900 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌)(le‘𝐾)𝑌) |
55 | 39, 40, 41, 54 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → (𝑋 ∧ 𝑌)(le‘𝐾)𝑌) |
56 | 55 | biantrurd 528 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → (𝑝(le‘𝐾)𝑌 ↔ ((𝑋 ∧ 𝑌)(le‘𝐾)𝑌 ∧ 𝑝(le‘𝐾)𝑌))) |
57 | 2, 11, 33 | latjle12 16885 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ Lat ∧ ((𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((𝑋 ∧ 𝑌)(le‘𝐾)𝑌 ∧ 𝑝(le‘𝐾)𝑌) ↔ ((𝑋 ∧ 𝑌) ∨ 𝑝)(le‘𝐾)𝑌)) |
58 | 39, 42, 43, 41, 57 | syl13anc 1320 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → (((𝑋 ∧ 𝑌)(le‘𝐾)𝑌 ∧ 𝑝(le‘𝐾)𝑌) ↔ ((𝑋 ∧ 𝑌) ∨ 𝑝)(le‘𝐾)𝑌)) |
59 | 56, 58 | bitrd 267 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → (𝑝(le‘𝐾)𝑌 ↔ ((𝑋 ∧ 𝑌) ∨ 𝑝)(le‘𝐾)𝑌)) |
60 | 53, 59 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → ((¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌) ↔ ((𝑋 ∧ 𝑌)(lt‘𝐾)((𝑋 ∧ 𝑌) ∨ 𝑝) ∧ ((𝑋 ∧ 𝑌) ∨ 𝑝)(le‘𝐾)𝑌))) |
61 | | hlpos 33670 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset) |
62 | 38, 61 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → 𝐾 ∈ Poset) |
63 | 2, 33 | latjcl 16874 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑝 ∈ 𝐵) → ((𝑋 ∧ 𝑌) ∨ 𝑝) ∈ 𝐵) |
64 | 39, 42, 43, 63 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → ((𝑋 ∧ 𝑌) ∨ 𝑝) ∈ 𝐵) |
65 | 42, 41, 64 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → ((𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ((𝑋 ∧ 𝑌) ∨ 𝑝) ∈ 𝐵)) |
66 | 2, 11, 6, 7 | cvrnbtwn2 33580 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ Poset ∧ ((𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ((𝑋 ∧ 𝑌) ∨ 𝑝) ∈ 𝐵) ∧ (𝑋 ∧ 𝑌)𝐶𝑌) → (((𝑋 ∧ 𝑌)(lt‘𝐾)((𝑋 ∧ 𝑌) ∨ 𝑝) ∧ ((𝑋 ∧ 𝑌) ∨ 𝑝)(le‘𝐾)𝑌) ↔ ((𝑋 ∧ 𝑌) ∨ 𝑝) = 𝑌)) |
67 | 66 | biimpd 218 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ Poset ∧ ((𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ((𝑋 ∧ 𝑌) ∨ 𝑝) ∈ 𝐵) ∧ (𝑋 ∧ 𝑌)𝐶𝑌) → (((𝑋 ∧ 𝑌)(lt‘𝐾)((𝑋 ∧ 𝑌) ∨ 𝑝) ∧ ((𝑋 ∧ 𝑌) ∨ 𝑝)(le‘𝐾)𝑌) → ((𝑋 ∧ 𝑌) ∨ 𝑝) = 𝑌)) |
68 | 67 | 3exp 1256 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ Poset → (((𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ((𝑋 ∧ 𝑌) ∨ 𝑝) ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 → (((𝑋 ∧ 𝑌)(lt‘𝐾)((𝑋 ∧ 𝑌) ∨ 𝑝) ∧ ((𝑋 ∧ 𝑌) ∨ 𝑝)(le‘𝐾)𝑌) → ((𝑋 ∧ 𝑌) ∨ 𝑝) = 𝑌)))) |
69 | 62, 65, 68 | sylc 63 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 → (((𝑋 ∧ 𝑌)(lt‘𝐾)((𝑋 ∧ 𝑌) ∨ 𝑝) ∧ ((𝑋 ∧ 𝑌) ∨ 𝑝)(le‘𝐾)𝑌) → ((𝑋 ∧ 𝑌) ∨ 𝑝) = 𝑌))) |
70 | 69 | com23 84 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → (((𝑋 ∧ 𝑌)(lt‘𝐾)((𝑋 ∧ 𝑌) ∨ 𝑝) ∧ ((𝑋 ∧ 𝑌) ∨ 𝑝)(le‘𝐾)𝑌) → ((𝑋 ∧ 𝑌)𝐶𝑌 → ((𝑋 ∧ 𝑌) ∨ 𝑝) = 𝑌))) |
71 | 60, 70 | sylbid 229 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → ((¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌) → ((𝑋 ∧ 𝑌)𝐶𝑌 → ((𝑋 ∧ 𝑌) ∨ 𝑝) = 𝑌))) |
72 | 71 | com23 84 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 → ((¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌) → ((𝑋 ∧ 𝑌) ∨ 𝑝) = 𝑌))) |
73 | 72 | imp32 448 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) ∧ ((𝑋 ∧ 𝑌)𝐶𝑌 ∧ (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌))) → ((𝑋 ∧ 𝑌) ∨ 𝑝) = 𝑌) |
74 | 73 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) ∧ ((𝑋 ∧ 𝑌)𝐶𝑌 ∧ (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌))) → (𝑋 ∨ ((𝑋 ∧ 𝑌) ∨ 𝑝)) = (𝑋 ∨ 𝑌)) |
75 | 51, 74 | eqtr3d 2646 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐵) ∧ ((𝑋 ∧ 𝑌)𝐶𝑌 ∧ (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌))) → (𝑋 ∨ 𝑝) = (𝑋 ∨ 𝑌)) |
76 | 19, 75 | sylanl2 681 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) ∧ ((𝑋 ∧ 𝑌)𝐶𝑌 ∧ (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌))) → (𝑋 ∨ 𝑝) = (𝑋 ∨ 𝑌)) |
77 | 37, 76 | breqtrd 4609 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) ∧ ((𝑋 ∧ 𝑌)𝐶𝑌 ∧ (¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌))) → 𝑋𝐶(𝑋 ∨ 𝑌)) |
78 | 77 | expr 641 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ (Atoms‘𝐾)) ∧ (𝑋 ∧ 𝑌)𝐶𝑌) → ((¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌) → 𝑋𝐶(𝑋 ∨ 𝑌))) |
79 | 78 | an32s 842 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌)𝐶𝑌) ∧ 𝑝 ∈ (Atoms‘𝐾)) → ((¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌) → 𝑋𝐶(𝑋 ∨ 𝑌))) |
80 | 79 | rexlimdva 3013 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌)𝐶𝑌) → (∃𝑝 ∈ (Atoms‘𝐾)(¬ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ 𝑝(le‘𝐾)𝑌) → 𝑋𝐶(𝑋 ∨ 𝑌))) |
81 | 16, 80 | mpd 15 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌)𝐶𝑌) → 𝑋𝐶(𝑋 ∨ 𝑌)) |
82 | 81 | ex 449 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 → 𝑋𝐶(𝑋 ∨ 𝑌))) |