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 |
| 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 |