This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem glbeldm

Description: Member of the domain of the greatest lower bound function of a poset. (Contributed by NM, 7-Sep-2018)

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

Proof

Step Hyp Ref Expression
1 glbeldm.b 
 |-  B = ( Base ` K )
2 glbeldm.l 
 |-  .<_ = ( le ` K )
3 glbeldm.g 
 |-  G = ( glb ` K )
4 glbeldm.p 
 |-  ( ps <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
5 glbeldm.k 
 |-  ( ph -> K e. V )
6 biid 
 |-  ( ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) <-> ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) )
7 1 2 3 6 5 glbdm 
 |-  ( ph -> dom G = { s e. ~P B | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) } )
8 7 eleq2d 
 |-  ( ph -> ( S e. dom G <-> S e. { s e. ~P B | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) } ) )
9 raleq 
 |-  ( s = S -> ( A. y e. s x .<_ y <-> A. y e. S x .<_ y ) )
10 raleq 
 |-  ( s = S -> ( A. y e. s z .<_ y <-> A. y e. S z .<_ y ) )
11 10 imbi1d 
 |-  ( s = S -> ( ( A. y e. s z .<_ y -> z .<_ x ) <-> ( A. y e. S z .<_ y -> z .<_ x ) ) )
12 11 ralbidv 
 |-  ( s = S -> ( A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) <-> A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
13 9 12 anbi12d 
 |-  ( s = S -> ( ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) ) )
14 13 reubidv 
 |-  ( s = S -> ( E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) <-> E! x e. B ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) ) )
15 4 reubii 
 |-  ( 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 bitr4di 
 |-  ( s = S -> ( E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) <-> E! x e. B ps ) )
17 16 elrab 
 |-  ( S e. { s e. ~P B | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) } <-> ( S e. ~P B /\ E! x e. B ps ) )
18 1 fvexi 
 |-  B e. _V
19 18 elpw2 
 |-  ( S e. ~P B <-> S C_ B )
20 19 anbi1i 
 |-  ( ( S e. ~P B /\ E! x e. B ps ) <-> ( S C_ B /\ E! x e. B ps ) )
21 17 20 bitri 
 |-  ( S e. { s e. ~P B | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) } <-> ( S C_ B /\ E! x e. B ps ) )
22 8 21 bitrdi 
 |-  ( ph -> ( S e. dom G <-> ( S C_ B /\ E! x e. B ps ) ) )