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 ` K )
posglbdg.b
|- ( ph -> B = ( Base ` K ) )
posglbdg.g
|- ( ph -> G = ( glb ` K ) )
posglbdg.k
|- ( ph -> K e. Poset )
posglbdg.s
|- ( ph -> S C_ B )
posglbdg.t
|- ( ph -> T e. B )
posglbdg.lb
|- ( ( ph /\ x e. S ) -> T .<_ x )
posglbdg.gt
|- ( ( ph /\ y e. B /\ A. x e. S y .<_ x ) -> y .<_ T )
Assertion posglbdg
|- ( ph -> ( G ` S ) = T )

Proof

Step Hyp Ref Expression
1 posglbdg.l
 |-  .<_ = ( le ` K )
2 posglbdg.b
 |-  ( ph -> B = ( Base ` K ) )
3 posglbdg.g
 |-  ( ph -> G = ( glb ` K ) )
4 posglbdg.k
 |-  ( ph -> K e. Poset )
5 posglbdg.s
 |-  ( ph -> S C_ B )
6 posglbdg.t
 |-  ( ph -> T e. B )
7 posglbdg.lb
 |-  ( ( ph /\ x e. S ) -> T .<_ x )
8 posglbdg.gt
 |-  ( ( ph /\ y e. B /\ A. x e. S y .<_ x ) -> y .<_ T )
9 eqid
 |-  ( ODual ` K ) = ( ODual ` K )
10 9 1 oduleval
 |-  `' .<_ = ( le ` ( ODual ` K ) )
11 eqid
 |-  ( Base ` K ) = ( Base ` K )
12 9 11 odubas
 |-  ( Base ` K ) = ( Base ` ( ODual ` K ) )
13 2 12 eqtrdi
 |-  ( ph -> B = ( Base ` ( ODual ` K ) ) )
14 eqid
 |-  ( glb ` K ) = ( glb ` K )
15 9 14 odulub
 |-  ( K e. Poset -> ( glb ` K ) = ( lub ` ( ODual ` K ) ) )
16 4 15 syl
 |-  ( ph -> ( glb ` K ) = ( lub ` ( ODual ` K ) ) )
17 3 16 eqtrd
 |-  ( ph -> G = ( lub ` ( ODual ` K ) ) )
18 9 odupos
 |-  ( K e. Poset -> ( ODual ` K ) e. Poset )
19 4 18 syl
 |-  ( ph -> ( ODual ` K ) e. Poset )
20 vex
 |-  x e. _V
21 brcnvg
 |-  ( ( x e. _V /\ T e. B ) -> ( x `' .<_ T <-> T .<_ x ) )
22 20 6 21 sylancr
 |-  ( ph -> ( x `' .<_ T <-> T .<_ x ) )
23 22 adantr
 |-  ( ( ph /\ x e. S ) -> ( x `' .<_ T <-> T .<_ x ) )
24 7 23 mpbird
 |-  ( ( ph /\ x e. S ) -> x `' .<_ T )
25 vex
 |-  y e. _V
26 20 25 brcnv
 |-  ( x `' .<_ y <-> y .<_ x )
27 26 ralbii
 |-  ( A. x e. S x `' .<_ y <-> A. x e. S y .<_ x )
28 27 8 syl3an3b
 |-  ( ( ph /\ y e. B /\ A. x e. S x `' .<_ y ) -> y .<_ T )
29 brcnvg
 |-  ( ( T e. B /\ y e. _V ) -> ( T `' .<_ y <-> y .<_ T ) )
30 6 25 29 sylancl
 |-  ( ph -> ( T `' .<_ y <-> y .<_ T ) )
31 30 3ad2ant1
 |-  ( ( ph /\ y e. B /\ A. x e. S x `' .<_ y ) -> ( T `' .<_ y <-> y .<_ T ) )
32 28 31 mpbird
 |-  ( ( ph /\ y e. B /\ A. x e. S x `' .<_ y ) -> T `' .<_ y )
33 10 13 17 19 5 6 24 32 poslubdg
 |-  ( ph -> ( G ` S ) = T )