Description: An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of MaedaMaeda p. 30. ( chpssati , with /\ swapped, analog.) (Contributed by NM, 4-Dec-2011)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hlrelat1.b | |- B = ( Base ` K ) |
|
| hlrelat1.l | |- .<_ = ( le ` K ) |
||
| hlrelat1.s | |- .< = ( lt ` K ) |
||
| hlrelat1.a | |- A = ( Atoms ` K ) |
||
| Assertion | hlrelat1 | |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .< Y -> E. p e. A ( -. p .<_ X /\ p .<_ Y ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hlrelat1.b | |- B = ( Base ` K ) |
|
| 2 | hlrelat1.l | |- .<_ = ( le ` K ) |
|
| 3 | hlrelat1.s | |- .< = ( lt ` K ) |
|
| 4 | hlrelat1.a | |- A = ( Atoms ` K ) |
|
| 5 | hlomcmat | |- ( K e. HL -> ( K e. OML /\ K e. CLat /\ K e. AtLat ) ) |
|
| 6 | 1 2 3 4 | atlrelat1 | |- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( X .< Y -> E. p e. A ( -. p .<_ X /\ p .<_ Y ) ) ) |
| 7 | 5 6 | syl3an1 | |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .< Y -> E. p e. A ( -. p .<_ X /\ p .<_ Y ) ) ) |