| Step |
Hyp |
Ref |
Expression |
| 1 |
|
posglbdg.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
| 2 |
|
posglbdg.b |
⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) ) |
| 3 |
|
posglbdg.g |
⊢ ( 𝜑 → 𝐺 = ( glb ‘ 𝐾 ) ) |
| 4 |
|
posglbdg.k |
⊢ ( 𝜑 → 𝐾 ∈ Poset ) |
| 5 |
|
posglbdg.s |
⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 ) |
| 6 |
|
posglbdg.t |
⊢ ( 𝜑 → 𝑇 ∈ 𝐵 ) |
| 7 |
|
posglbdg.lb |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑇 ≤ 𝑥 ) |
| 8 |
|
posglbdg.gt |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 𝑦 ≤ 𝑥 ) → 𝑦 ≤ 𝑇 ) |
| 9 |
|
eqid |
⊢ ( ODual ‘ 𝐾 ) = ( ODual ‘ 𝐾 ) |
| 10 |
9 1
|
oduleval |
⊢ ◡ ≤ = ( le ‘ ( ODual ‘ 𝐾 ) ) |
| 11 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
| 12 |
9 11
|
odubas |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ ( ODual ‘ 𝐾 ) ) |
| 13 |
2 12
|
eqtrdi |
⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( ODual ‘ 𝐾 ) ) ) |
| 14 |
|
eqid |
⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 ) |
| 15 |
9 14
|
odulub |
⊢ ( 𝐾 ∈ Poset → ( glb ‘ 𝐾 ) = ( lub ‘ ( ODual ‘ 𝐾 ) ) ) |
| 16 |
4 15
|
syl |
⊢ ( 𝜑 → ( glb ‘ 𝐾 ) = ( lub ‘ ( ODual ‘ 𝐾 ) ) ) |
| 17 |
3 16
|
eqtrd |
⊢ ( 𝜑 → 𝐺 = ( lub ‘ ( ODual ‘ 𝐾 ) ) ) |
| 18 |
9
|
odupos |
⊢ ( 𝐾 ∈ Poset → ( ODual ‘ 𝐾 ) ∈ Poset ) |
| 19 |
4 18
|
syl |
⊢ ( 𝜑 → ( ODual ‘ 𝐾 ) ∈ Poset ) |
| 20 |
|
vex |
⊢ 𝑥 ∈ V |
| 21 |
|
brcnvg |
⊢ ( ( 𝑥 ∈ V ∧ 𝑇 ∈ 𝐵 ) → ( 𝑥 ◡ ≤ 𝑇 ↔ 𝑇 ≤ 𝑥 ) ) |
| 22 |
20 6 21
|
sylancr |
⊢ ( 𝜑 → ( 𝑥 ◡ ≤ 𝑇 ↔ 𝑇 ≤ 𝑥 ) ) |
| 23 |
22
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ◡ ≤ 𝑇 ↔ 𝑇 ≤ 𝑥 ) ) |
| 24 |
7 23
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ◡ ≤ 𝑇 ) |
| 25 |
|
vex |
⊢ 𝑦 ∈ V |
| 26 |
20 25
|
brcnv |
⊢ ( 𝑥 ◡ ≤ 𝑦 ↔ 𝑦 ≤ 𝑥 ) |
| 27 |
26
|
ralbii |
⊢ ( ∀ 𝑥 ∈ 𝑆 𝑥 ◡ ≤ 𝑦 ↔ ∀ 𝑥 ∈ 𝑆 𝑦 ≤ 𝑥 ) |
| 28 |
27 8
|
syl3an3b |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 ◡ ≤ 𝑦 ) → 𝑦 ≤ 𝑇 ) |
| 29 |
|
brcnvg |
⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑦 ∈ V ) → ( 𝑇 ◡ ≤ 𝑦 ↔ 𝑦 ≤ 𝑇 ) ) |
| 30 |
6 25 29
|
sylancl |
⊢ ( 𝜑 → ( 𝑇 ◡ ≤ 𝑦 ↔ 𝑦 ≤ 𝑇 ) ) |
| 31 |
30
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 ◡ ≤ 𝑦 ) → ( 𝑇 ◡ ≤ 𝑦 ↔ 𝑦 ≤ 𝑇 ) ) |
| 32 |
28 31
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 ◡ ≤ 𝑦 ) → 𝑇 ◡ ≤ 𝑦 ) |
| 33 |
10 13 17 19 5 6 24 32
|
poslubdg |
⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) = 𝑇 ) |