Step |
Hyp |
Ref |
Expression |
1 |
|
atlex.b |
|- B = ( Base ` K ) |
2 |
|
atlex.l |
|- .<_ = ( le ` K ) |
3 |
|
atlex.z |
|- .0. = ( 0. ` K ) |
4 |
|
atlex.a |
|- A = ( Atoms ` K ) |
5 |
|
eqid |
|- ( glb ` K ) = ( glb ` K ) |
6 |
1 5 2 3 4
|
isatl |
|- ( K e. AtLat <-> ( K e. Lat /\ B e. dom ( glb ` K ) /\ A. x e. B ( x =/= .0. -> E. y e. A y .<_ x ) ) ) |
7 |
6
|
simp3bi |
|- ( K e. AtLat -> A. x e. B ( x =/= .0. -> E. y e. A y .<_ x ) ) |
8 |
|
neeq1 |
|- ( x = X -> ( x =/= .0. <-> X =/= .0. ) ) |
9 |
|
breq2 |
|- ( x = X -> ( y .<_ x <-> y .<_ X ) ) |
10 |
9
|
rexbidv |
|- ( x = X -> ( E. y e. A y .<_ x <-> E. y e. A y .<_ X ) ) |
11 |
8 10
|
imbi12d |
|- ( x = X -> ( ( x =/= .0. -> E. y e. A y .<_ x ) <-> ( X =/= .0. -> E. y e. A y .<_ X ) ) ) |
12 |
11
|
rspccv |
|- ( A. x e. B ( x =/= .0. -> E. y e. A y .<_ x ) -> ( X e. B -> ( X =/= .0. -> E. y e. A y .<_ X ) ) ) |
13 |
7 12
|
syl |
|- ( K e. AtLat -> ( X e. B -> ( X =/= .0. -> E. y e. A y .<_ X ) ) ) |
14 |
13
|
3imp |
|- ( ( K e. AtLat /\ X e. B /\ X =/= .0. ) -> E. y e. A y .<_ X ) |