This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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