Metamath Proof Explorer

Theorem glbeldm2

Description: Member of the domain of the greatest lower bound function of a poset. (Contributed by Zhi Wang, 26-Sep-2024)

Ref Expression
Hypotheses lubeldm2.b 
|- B = ( Base ` K )
lubeldm2.l 
|- .<_ = ( le ` K )
glbeldm2.g 
|- G = ( glb ` K )
glbeldm2.p 
|- ( ps <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
glbeldm2.k 
|- ( ph -> K e. Poset )
Assertion glbeldm2 
|- ( ph -> ( S e. dom G <-> ( S C_ B /\ E. x e. B ps ) ) )

Proof

Step Hyp Ref Expression
1 lubeldm2.b 
 |-  B = ( Base ` K )
2 lubeldm2.l 
 |-  .<_ = ( le ` K )
3 glbeldm2.g 
 |-  G = ( glb ` K )
4 glbeldm2.p 
 |-  ( ps <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
5 glbeldm2.k 
 |-  ( ph -> K e. Poset )
6 1 2 3 4 5 glbeldm 
 |-  ( ph -> ( S e. dom G <-> ( S C_ B /\ E! x e. B ps ) ) )
7 6 biimpa 
 |-  ( ( ph /\ S e. dom G ) -> ( S C_ B /\ E! x e. B ps ) )
8 reurex 
 |-  ( E! x e. B ps -> E. x e. B ps )
9 8 anim2i 
 |-  ( ( S C_ B /\ E! x e. B ps ) -> ( S C_ B /\ E. x e. B ps ) )
10 7 9 syl 
 |-  ( ( ph /\ S e. dom G ) -> ( S C_ B /\ E. x e. B ps ) )
11 simpl 
 |-  ( ( ph /\ ( S C_ B /\ E. x e. B ps ) ) -> ph )
12 simprl 
 |-  ( ( ph /\ ( S C_ B /\ E. x e. B ps ) ) -> S C_ B )
13 2 1 posglbmo 
 |-  ( ( K e. Poset /\ S C_ B ) -> E* x e. B ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
14 5 13 sylan 
 |-  ( ( ph /\ S C_ B ) -> E* x e. B ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
15 4 rmobii 
 |-  ( E* x e. B ps <-> E* x e. B ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
16 14 15 sylibr 
 |-  ( ( ph /\ S C_ B ) -> E* x e. B ps )
17 16 anim1ci 
 |-  ( ( ( ph /\ S C_ B ) /\ E. x e. B ps ) -> ( E. x e. B ps /\ E* x e. B ps ) )
18 reu5 
 |-  ( E! x e. B ps <-> ( E. x e. B ps /\ E* x e. B ps ) )
19 17 18 sylibr 
 |-  ( ( ( ph /\ S C_ B ) /\ E. x e. B ps ) -> E! x e. B ps )
20 19 anasss 
 |-  ( ( ph /\ ( S C_ B /\ E. x e. B ps ) ) -> E! x e. B ps )
21 6 biimpar 
 |-  ( ( ph /\ ( S C_ B /\ E! x e. B ps ) ) -> S e. dom G )
22 11 12 20 21 syl12anc 
 |-  ( ( ph /\ ( S C_ B /\ E. x e. B ps ) ) -> S e. dom G )
23 10 22 impbida 
 |-  ( ph -> ( S e. dom G <-> ( S C_ B /\ E. x e. B ps ) ) )