# Metamath Proof Explorer

## Theorem isomliN

Description: Properties that determine an orthomodular lattice. (Contributed by NM, 18-Sep-2011) (New usage is discouraged.)

Ref Expression
Hypotheses isomli.0
`|- K e. OL`
isomli.b
`|- B = ( Base ` K )`
isomli.l
`|- .<_ = ( le ` K )`
isomli.j
`|- .\/ = ( join ` K )`
isomli.m
`|- ./\ = ( meet ` K )`
isomli.o
`|- ._|_ = ( oc ` K )`
isomli.7
`|- ( ( x e. B /\ y e. B ) -> ( x .<_ y -> y = ( x .\/ ( y ./\ ( ._|_ ` x ) ) ) ) )`
Assertion isomliN
`|- K e. OML`

### Proof

Step Hyp Ref Expression
1 isomli.0
` |-  K e. OL`
2 isomli.b
` |-  B = ( Base ` K )`
3 isomli.l
` |-  .<_ = ( le ` K )`
4 isomli.j
` |-  .\/ = ( join ` K )`
5 isomli.m
` |-  ./\ = ( meet ` K )`
6 isomli.o
` |-  ._|_ = ( oc ` K )`
7 isomli.7
` |-  ( ( x e. B /\ y e. B ) -> ( x .<_ y -> y = ( x .\/ ( y ./\ ( ._|_ ` x ) ) ) ) )`
8 7 rgen2
` |-  A. x e. B A. y e. B ( x .<_ y -> y = ( x .\/ ( y ./\ ( ._|_ ` x ) ) ) )`
9 2 3 4 5 6 isoml
` |-  ( K e. OML <-> ( K e. OL /\ A. x e. B A. y e. B ( x .<_ y -> y = ( x .\/ ( y ./\ ( ._|_ ` x ) ) ) ) ) )`
10 1 8 9 mpbir2an
` |-  K e. OML`