Description: The predicate "is a co-atom (lattice hyperplane)". (Contributed by NM, 11-May-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lhpset.b | |- B = ( Base ` K ) |
|
lhpset.u | |- .1. = ( 1. ` K ) |
||
lhpset.c | |- C = ( |
||
lhpset.h | |- H = ( LHyp ` K ) |
||
Assertion | islhp | |- ( K e. A -> ( W e. H <-> ( W e. B /\ W C .1. ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lhpset.b | |- B = ( Base ` K ) |
|
2 | lhpset.u | |- .1. = ( 1. ` K ) |
|
3 | lhpset.c | |- C = ( |
|
4 | lhpset.h | |- H = ( LHyp ` K ) |
|
5 | 1 2 3 4 | lhpset | |- ( K e. A -> H = { w e. B | w C .1. } ) |
6 | 5 | eleq2d | |- ( K e. A -> ( W e. H <-> W e. { w e. B | w C .1. } ) ) |
7 | breq1 | |- ( w = W -> ( w C .1. <-> W C .1. ) ) |
|
8 | 7 | elrab | |- ( W e. { w e. B | w C .1. } <-> ( W e. B /\ W C .1. ) ) |
9 | 6 8 | bitrdi | |- ( K e. A -> ( W e. H <-> ( W e. B /\ W C .1. ) ) ) |