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