# Metamath Proof Explorer

## Theorem cvr2N

Description: Less-than and covers equivalence in a Hilbert lattice. ( chcv2 analog.) (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cvr2.b
`|- B = ( Base ` K )`
cvr2.s
`|- .< = ( lt ` K )`
cvr2.j
`|- .\/ = ( join ` K )`
cvr2.c
`|- C = ( `
cvr2.a
`|- A = ( Atoms ` K )`
Assertion cvr2N
`|- ( ( K e. HL /\ X e. B /\ P e. A ) -> ( X .< ( X .\/ P ) <-> X C ( X .\/ P ) ) )`

### Proof

Step Hyp Ref Expression
1 cvr2.b
` |-  B = ( Base ` K )`
2 cvr2.s
` |-  .< = ( lt ` K )`
3 cvr2.j
` |-  .\/ = ( join ` K )`
4 cvr2.c
` |-  C = ( `
5 cvr2.a
` |-  A = ( Atoms ` K )`
6 hllat
` |-  ( K e. HL -> K e. Lat )`
` |-  ( ( K e. HL /\ X e. B /\ P e. A ) -> K e. Lat )`
8 simp2
` |-  ( ( K e. HL /\ X e. B /\ P e. A ) -> X e. B )`
9 1 5 atbase
` |-  ( P e. A -> P e. B )`
` |-  ( ( K e. HL /\ X e. B /\ P e. A ) -> P e. B )`
` |-  ( le ` K ) = ( le ` K )`
` |-  ( ( K e. Lat /\ X e. B /\ P e. B ) -> ( -. P ( le ` K ) X <-> X .< ( X .\/ P ) ) )`
` |-  ( ( K e. HL /\ X e. B /\ P e. A ) -> ( -. P ( le ` K ) X <-> X .< ( X .\/ P ) ) )`
` |-  ( ( K e. HL /\ X e. B /\ P e. A ) -> ( -. P ( le ` K ) X <-> X C ( X .\/ P ) ) )`
` |-  ( ( K e. HL /\ X e. B /\ P e. A ) -> ( X .< ( X .\/ P ) <-> X C ( X .\/ P ) ) )`