Step | Hyp | Ref
| Expression |
1 | | clatglb.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
2 | | clatglb.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
3 | | clatglb.g |
. . . . . . 7
⊢ 𝐺 = (glb‘𝐾) |
4 | 1, 2, 3 | clatglble 18023 |
. . . . . 6
⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑦 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑦) |
5 | 4 | 3expa 1120 |
. . . . 5
⊢ (((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) ∧ 𝑦 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑦) |
6 | 5 | 3adantl2 1169 |
. . . 4
⊢ (((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) ∧ 𝑦 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑦) |
7 | | simpl1 1193 |
. . . . . 6
⊢ (((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) ∧ 𝑦 ∈ 𝑆) → 𝐾 ∈ CLat) |
8 | | clatl 18014 |
. . . . . 6
⊢ (𝐾 ∈ CLat → 𝐾 ∈ Lat) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) ∧ 𝑦 ∈ 𝑆) → 𝐾 ∈ Lat) |
10 | | simpl2 1194 |
. . . . 5
⊢ (((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) ∧ 𝑦 ∈ 𝑆) → 𝑋 ∈ 𝐵) |
11 | 1, 3 | clatglbcl 18011 |
. . . . . . 7
⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵) |
12 | 11 | 3adant2 1133 |
. . . . . 6
⊢ ((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵) |
13 | 12 | adantr 484 |
. . . . 5
⊢ (((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) ∧ 𝑦 ∈ 𝑆) → (𝐺‘𝑆) ∈ 𝐵) |
14 | | ssel 3893 |
. . . . . . 7
⊢ (𝑆 ⊆ 𝐵 → (𝑦 ∈ 𝑆 → 𝑦 ∈ 𝐵)) |
15 | 14 | 3ad2ant3 1137 |
. . . . . 6
⊢ ((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → (𝑦 ∈ 𝑆 → 𝑦 ∈ 𝐵)) |
16 | 15 | imp 410 |
. . . . 5
⊢ (((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝐵) |
17 | 1, 2 | lattr 17950 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ (𝐺‘𝑆) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑋 ≤ (𝐺‘𝑆) ∧ (𝐺‘𝑆) ≤ 𝑦) → 𝑋 ≤ 𝑦)) |
18 | 9, 10, 13, 16, 17 | syl13anc 1374 |
. . . 4
⊢ (((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) ∧ 𝑦 ∈ 𝑆) → ((𝑋 ≤ (𝐺‘𝑆) ∧ (𝐺‘𝑆) ≤ 𝑦) → 𝑋 ≤ 𝑦)) |
19 | 6, 18 | mpan2d 694 |
. . 3
⊢ (((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) ∧ 𝑦 ∈ 𝑆) → (𝑋 ≤ (𝐺‘𝑆) → 𝑋 ≤ 𝑦)) |
20 | 19 | ralrimdva 3110 |
. 2
⊢ ((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → (𝑋 ≤ (𝐺‘𝑆) → ∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦)) |
21 | 1, 2, 3 | clatglb 18022 |
. . . . . 6
⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 (𝐺‘𝑆) ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝐺‘𝑆)))) |
22 | | breq1 5056 |
. . . . . . . . 9
⊢ (𝑧 = 𝑋 → (𝑧 ≤ 𝑦 ↔ 𝑋 ≤ 𝑦)) |
23 | 22 | ralbidv 3118 |
. . . . . . . 8
⊢ (𝑧 = 𝑋 → (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 ↔ ∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦)) |
24 | | breq1 5056 |
. . . . . . . 8
⊢ (𝑧 = 𝑋 → (𝑧 ≤ (𝐺‘𝑆) ↔ 𝑋 ≤ (𝐺‘𝑆))) |
25 | 23, 24 | imbi12d 348 |
. . . . . . 7
⊢ (𝑧 = 𝑋 → ((∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝐺‘𝑆)) ↔ (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 → 𝑋 ≤ (𝐺‘𝑆)))) |
26 | 25 | rspccv 3534 |
. . . . . 6
⊢
(∀𝑧 ∈
𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝐺‘𝑆)) → (𝑋 ∈ 𝐵 → (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 → 𝑋 ≤ (𝐺‘𝑆)))) |
27 | 21, 26 | simpl2im 507 |
. . . . 5
⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝑋 ∈ 𝐵 → (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 → 𝑋 ≤ (𝐺‘𝑆)))) |
28 | 27 | ex 416 |
. . . 4
⊢ (𝐾 ∈ CLat → (𝑆 ⊆ 𝐵 → (𝑋 ∈ 𝐵 → (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 → 𝑋 ≤ (𝐺‘𝑆))))) |
29 | 28 | com23 86 |
. . 3
⊢ (𝐾 ∈ CLat → (𝑋 ∈ 𝐵 → (𝑆 ⊆ 𝐵 → (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 → 𝑋 ≤ (𝐺‘𝑆))))) |
30 | 29 | 3imp 1113 |
. 2
⊢ ((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 → 𝑋 ≤ (𝐺‘𝑆))) |
31 | 20, 30 | impbid 215 |
1
⊢ ((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → (𝑋 ≤ (𝐺‘𝑆) ↔ ∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦)) |