Metamath Proof Explorer

Theorem glbprlem

Description: Lemma for glbprdm and glbpr . (Contributed by Zhi Wang, 26-Sep-2024)

Ref Expression
Hypotheses lubpr.k 
|- ( ph -> K e. Poset )
lubpr.b 
|- B = ( Base ` K )
lubpr.x 
|- ( ph -> X e. B )
lubpr.y 
|- ( ph -> Y e. B )
lubpr.l 
|- .<_ = ( le ` K )
lubpr.c 
|- ( ph -> X .<_ Y )
lubpr.s 
|- ( ph -> S = { X , Y } )
glbpr.g 
|- G = ( glb ` K )
Assertion glbprlem 
|- ( ph -> ( S e. dom G /\ ( G ` S ) = X ) )

Proof

Step Hyp Ref Expression
1 lubpr.k 
 |-  ( ph -> K e. Poset )
2 lubpr.b 
 |-  B = ( Base ` K )
3 lubpr.x 
 |-  ( ph -> X e. B )
4 lubpr.y 
 |-  ( ph -> Y e. B )
5 lubpr.l 
 |-  .<_ = ( le ` K )
6 lubpr.c 
 |-  ( ph -> X .<_ Y )
7 lubpr.s 
 |-  ( ph -> S = { X , Y } )
8 glbpr.g 
 |-  G = ( glb ` K )
9 eqid 
 |-  ( ODual ` K ) = ( ODual ` K )
10 9 odupos 
 |-  ( K e. Poset -> ( ODual ` K ) e. Poset )
11 1 10 syl 
 |-  ( ph -> ( ODual ` K ) e. Poset )
12 9 2 odubas 
 |-  B = ( Base ` ( ODual ` K ) )
13 9 5 oduleval 
 |-  `' .<_ = ( le ` ( ODual ` K ) )
14 brcnvg 
 |-  ( ( Y e. B /\ X e. B ) -> ( Y `' .<_ X <-> X .<_ Y ) )
15 4 3 14 syl2anc 
 |-  ( ph -> ( Y `' .<_ X <-> X .<_ Y ) )
16 6 15 mpbird 
 |-  ( ph -> Y `' .<_ X )
17 prcom 
 |-  { X , Y } = { Y , X }
18 7 17 eqtrdi 
 |-  ( ph -> S = { Y , X } )
19 eqid 
 |-  ( lub ` ( ODual ` K ) ) = ( lub ` ( ODual ` K ) )
20 11 12 4 3 13 16 18 19 lubprdm 
 |-  ( ph -> S e. dom ( lub ` ( ODual ` K ) ) )
21 9 8 odulub 
 |-  ( K e. Poset -> G = ( lub ` ( ODual ` K ) ) )
22 1 21 syl 
 |-  ( ph -> G = ( lub ` ( ODual ` K ) ) )
23 22 dmeqd 
 |-  ( ph -> dom G = dom ( lub ` ( ODual ` K ) ) )
24 20 23 eleqtrrd 
 |-  ( ph -> S e. dom G )
25 22 fveq1d 
 |-  ( ph -> ( G ` S ) = ( ( lub ` ( ODual ` K ) ) ` S ) )
26 11 12 4 3 13 16 18 19 lubpr 
 |-  ( ph -> ( ( lub ` ( ODual ` K ) ) ` S ) = X )
27 25 26 eqtrd 
 |-  ( ph -> ( G ` S ) = X )
28 24 27 jca 
 |-  ( ph -> ( S e. dom G /\ ( G ` S ) = X ) )