Metamath Proof Explorer


Theorem posglbdg

Description: Properties which determine the greatest lower bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypotheses posglbdg.l = ( le ‘ 𝐾 )
posglbdg.b ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
posglbdg.g ( 𝜑𝐺 = ( glb ‘ 𝐾 ) )
posglbdg.k ( 𝜑𝐾 ∈ Poset )
posglbdg.s ( 𝜑𝑆𝐵 )
posglbdg.t ( 𝜑𝑇𝐵 )
posglbdg.lb ( ( 𝜑𝑥𝑆 ) → 𝑇 𝑥 )
posglbdg.gt ( ( 𝜑𝑦𝐵 ∧ ∀ 𝑥𝑆 𝑦 𝑥 ) → 𝑦 𝑇 )
Assertion posglbdg ( 𝜑 → ( 𝐺𝑆 ) = 𝑇 )

Proof

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 ( 𝜑 → ( 𝐺𝑆 ) = 𝑇 )