Proof of Theorem lecmtN
Step | Hyp | Ref
| Expression |
1 | | omllat 36993 |
. . . . 5
⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat) |
2 | 1 | 3ad2ant1 1135 |
. . . 4
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat) |
3 | | simp2 1139 |
. . . 4
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
4 | | omlop 36992 |
. . . . . . 7
⊢ (𝐾 ∈ OML → 𝐾 ∈ OP) |
5 | 4 | 3ad2ant1 1135 |
. . . . . 6
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OP) |
6 | | lecmt.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
7 | | eqid 2737 |
. . . . . . 7
⊢
(oc‘𝐾) =
(oc‘𝐾) |
8 | 6, 7 | opoccl 36945 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) |
9 | 5, 3, 8 | syl2anc 587 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) |
10 | | simp3 1140 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) |
11 | | eqid 2737 |
. . . . . 6
⊢
(join‘𝐾) =
(join‘𝐾) |
12 | 6, 11 | latjcl 17945 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧
((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵) |
13 | 2, 9, 10, 12 | syl3anc 1373 |
. . . 4
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵) |
14 | | lecmt.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
15 | | eqid 2737 |
. . . . 5
⊢
(meet‘𝐾) =
(meet‘𝐾) |
16 | 6, 14, 15 | latmle1 17970 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵) → (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑋) |
17 | 2, 3, 13, 16 | syl3anc 1373 |
. . 3
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑋) |
18 | 6, 15 | latmcl 17946 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵) → (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ∈ 𝐵) |
19 | 2, 3, 13, 18 | syl3anc 1373 |
. . . 4
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ∈ 𝐵) |
20 | 6, 14 | lattr 17950 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ ((𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑋 ∧ 𝑋 ≤ 𝑌) → (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑌)) |
21 | 2, 19, 3, 10, 20 | syl13anc 1374 |
. . 3
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑋 ∧ 𝑋 ≤ 𝑌) → (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑌)) |
22 | 17, 21 | mpand 695 |
. 2
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑌)) |
23 | | lecmt.c |
. . 3
⊢ 𝐶 = (cm‘𝐾) |
24 | 6, 14, 11, 15, 7, 23 | cmtbr4N 37006 |
. 2
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) ≤ 𝑌)) |
25 | 22, 24 | sylibrd 262 |
1
⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑋𝐶𝑌)) |