Description: The predicate "is an orthomodular lattice." (Contributed by NM, 18-Sep-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isoml.b | |
|
isoml.l | |
||
isoml.j | |
||
isoml.m | |
||
isoml.o | |
||
Assertion | isoml | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isoml.b | |
|
2 | isoml.l | |
|
3 | isoml.j | |
|
4 | isoml.m | |
|
5 | isoml.o | |
|
6 | fveq2 | |
|
7 | 6 1 | eqtr4di | |
8 | fveq2 | |
|
9 | 8 2 | eqtr4di | |
10 | 9 | breqd | |
11 | fveq2 | |
|
12 | 11 3 | eqtr4di | |
13 | eqidd | |
|
14 | fveq2 | |
|
15 | 14 4 | eqtr4di | |
16 | eqidd | |
|
17 | fveq2 | |
|
18 | 17 5 | eqtr4di | |
19 | 18 | fveq1d | |
20 | 15 16 19 | oveq123d | |
21 | 12 13 20 | oveq123d | |
22 | 21 | eqeq2d | |
23 | 10 22 | imbi12d | |
24 | 7 23 | raleqbidv | |
25 | 7 24 | raleqbidv | |
26 | df-oml | |
|
27 | 25 26 | elrab2 | |