Metamath Proof Explorer

Theorem glbeldm2d

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

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

Proof

Step Hyp Ref Expression
1 lubeldm2d.b 
 |-  ( ph -> B = ( Base ` K ) )
2 lubeldm2d.l 
 |-  ( ph -> .<_ = ( le ` K ) )
3 glbeldm2d.g 
 |-  ( ph -> G = ( glb ` K ) )
4 glbeldm2d.p 
 |-  ( ( ph /\ x e. B ) -> ( ps <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) ) )
5 glbeldm2d.k 
 |-  ( ph -> K e. Poset )
6 eqid 
 |-  ( Base ` K ) = ( Base ` K )
7 eqid 
 |-  ( le ` K ) = ( le ` K )
8 eqid 
 |-  ( glb ` K ) = ( glb ` K )
9 biid 
 |-  ( ( A. y e. S x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. S z ( le ` K ) y -> z ( le ` K ) x ) ) <-> ( A. y e. S x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. S z ( le ` K ) y -> z ( le ` K ) x ) ) )
10 6 7 8 9 5 glbeldm2 
 |-  ( ph -> ( S e. dom ( glb ` K ) <-> ( S C_ ( Base ` K ) /\ E. x e. ( Base ` K ) ( A. y e. S x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. S z ( le ` K ) y -> z ( le ` K ) x ) ) ) ) )
11 3 dmeqd 
 |-  ( ph -> dom G = dom ( glb ` K ) )
12 11 eleq2d 
 |-  ( ph -> ( S e. dom G <-> S e. dom ( glb ` K ) ) )
13 1 sseq2d 
 |-  ( ph -> ( S C_ B <-> S C_ ( Base ` K ) ) )
14 2 breqd 
 |-  ( ph -> ( x .<_ y <-> x ( le ` K ) y ) )
15 14 ralbidv 
 |-  ( ph -> ( A. y e. S x .<_ y <-> A. y e. S x ( le ` K ) y ) )
16 2 breqd 
 |-  ( ph -> ( z .<_ y <-> z ( le ` K ) y ) )
17 16 ralbidv 
 |-  ( ph -> ( A. y e. S z .<_ y <-> A. y e. S z ( le ` K ) y ) )
18 2 breqd 
 |-  ( ph -> ( z .<_ x <-> z ( le ` K ) x ) )
19 17 18 imbi12d 
 |-  ( ph -> ( ( A. y e. S z .<_ y -> z .<_ x ) <-> ( A. y e. S z ( le ` K ) y -> z ( le ` K ) x ) ) )
20 1 19 raleqbidv 
 |-  ( ph -> ( A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) <-> A. z e. ( Base ` K ) ( A. y e. S z ( le ` K ) y -> z ( le ` K ) x ) ) )
21 15 20 anbi12d 
 |-  ( ph -> ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) <-> ( A. y e. S x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. S z ( le ` K ) y -> z ( le ` K ) x ) ) ) )
22 21 adantr 
 |-  ( ( ph /\ x e. B ) -> ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) <-> ( A. y e. S x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. S z ( le ` K ) y -> z ( le ` K ) x ) ) ) )
23 4 22 bitrd 
 |-  ( ( ph /\ x e. B ) -> ( ps <-> ( A. y e. S x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. S z ( le ` K ) y -> z ( le ` K ) x ) ) ) )
24 23 pm5.32da 
 |-  ( ph -> ( ( x e. B /\ ps ) <-> ( x e. B /\ ( A. y e. S x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. S z ( le ` K ) y -> z ( le ` K ) x ) ) ) ) )
25 1 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( Base ` K ) ) )
26 25 anbi1d 
 |-  ( ph -> ( ( x e. B /\ ( A. y e. S x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. S z ( le ` K ) y -> z ( le ` K ) x ) ) ) <-> ( x e. ( Base ` K ) /\ ( A. y e. S x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. S z ( le ` K ) y -> z ( le ` K ) x ) ) ) ) )
27 24 26 bitrd 
 |-  ( ph -> ( ( x e. B /\ ps ) <-> ( x e. ( Base ` K ) /\ ( A. y e. S x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. S z ( le ` K ) y -> z ( le ` K ) x ) ) ) ) )
28 27 rexbidv2 
 |-  ( ph -> ( E. x e. B ps <-> E. x e. ( Base ` K ) ( A. y e. S x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. S z ( le ` K ) y -> z ( le ` K ) x ) ) ) )
29 13 28 anbi12d 
 |-  ( ph -> ( ( S C_ B /\ E. x e. B ps ) <-> ( S C_ ( Base ` K ) /\ E. x e. ( Base ` K ) ( A. y e. S x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. S z ( le ` K ) y -> z ( le ` K ) x ) ) ) ) )
30 10 12 29 3bitr4d 
 |-  ( ph -> ( S e. dom G <-> ( S C_ B /\ E. x e. B ps ) ) )