Metamath Proof Explorer

Theorem atmd

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 
|- ( ( A e. HAtoms /\ B e. CH ) -> A MH B )

Proof

Step Hyp Ref Expression
1 atdmd 
 |-  ( ( A e. HAtoms /\ x e. CH ) -> A MH* x )
2 1 ralrimiva 
 |-  ( A e. HAtoms -> A. x e. CH A MH* x )
3 atelch 
 |-  ( A e. HAtoms -> A e. CH )
4 mddmd2 
 |-  ( A e. CH -> ( A. x e. CH A MH x <-> A. x e. CH A MH* x ) )
5 3 4 syl 
 |-  ( A e. HAtoms -> ( A. x e. CH A MH x <-> A. x e. CH A MH* x ) )
6 2 5 mpbird 
 |-  ( A e. HAtoms -> A. x e. CH A MH x )
7 breq2 
 |-  ( x = B -> ( A MH x <-> A MH B ) )
8 7 rspcv 
 |-  ( B e. CH -> ( A. x e. CH A MH x -> A MH B ) )
9 6 8 mpan9 
 |-  ( ( A e. HAtoms /\ B e. CH ) -> A MH B )