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 ` 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 )