Description: Two Hilbert lattice elements have the modular pair property if the first is an atom. Theorem 7.6(b) of MaedaMaeda p. 31. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | atmd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | atdmd | |
|
2 | 1 | ralrimiva | |
3 | atelch | |
|
4 | mddmd2 | |
|
5 | 3 4 | syl | |
6 | 2 5 | mpbird | |
7 | breq2 | |
|
8 | 7 | rspcv | |
9 | 6 8 | mpan9 | |